Допустимость правил вывода и логические уравнения в модальных логиках, аксиоматизирующих доказуемость

В работе изучаются модальные логики Геделя–Леба (GL) и Соловая (S) – наименьшее и наибольшее модальные представления арифметических теорий. Доказана разрешимость проблемы распознавания допустимости правил вывода с параметрами (в частности, без параметров) в GL и S, т.е. получено положительное решение аналогов проблемы Фридмана. Доказано, что аналог проблемы Кузнецова о конечности базисов допустимых правил для S и GL решается отрицательно. Найдены алгоритмы, распознающие разрешимость в GL и S логических уравнений и строящие решения для них.