Разрешимость по допустимости модальной системы $\mathrm{Grz}$ и интуиционистской логики

Найден критерий допустимости правил в модальной системе $\mathrm{Grz}\rightleftharpoons\mathrm S4+\Box(\Box(p\supset\Box p)\supset p)\supset p$. На его основе построен алгоритм, распознающий допустимость правил в $\mathrm{Grz}$. Из доказанной разрешимости по допустимости $\mathrm{Grz}$ как следствие получено положительное решение проблемы Кузнецова–Фридмана об алгоритмической разрешимости проблемы допустимости в интуиционистской логике высказываний. Алгебраические аналоги полученных результатов – разрешимость универсальных теорий свободной псевдобулевой алгебры и свободной топобулевой алгебры многообразия алгебр, соответствующего системе $\mathrm{Grz}$. Элементарные теории данных свободных алгебр наследственно неразрешимы.
Библиография: 15 названий.