Критерий допустимости правил в модальной системе ${\rm S}4$ и интуиционистской логике

Найден критерий допустимости правил в модальной логике ${\rm S}4$, на основе которого построен алгоритм, распознающий допустимость правил в ${\rm S}4$. Доказано, что правило $A/B$ допустимо в интуиционистской логике $Int$ тогда и только тогда, когда допустимо в ${\rm S}4$. Поэтому из доказанной разрешимости допустимости в ${\rm S}4$ вытекает положительное решение проблемы Кузнецова–Фридмана о существовании алгоритма, распознающего допустимость правил в $Int$. В ходе доказательства устанавливается разрешимость универсальных теорий свободной алгебры замыканий и свободной псевдобулевой алгебры.