Семантические критерии допустимости правил вывода в логиках $\mathbf{S4}$ и $\mathbf{Int}$

Найдены семантические критерии допустимости правил вывода с параметрами (в частности, обычных правил без параметров) в логиках $\mathbf{S4}$ и $\mathbf{Int}$. Они связаны с проверкой истинности формул на последовательности конструктивных счетных моделей Крипке, и хотя и не имеют чисто алгоритмического характера, достаточно удобны в реальном исполнении. Приводятся примеры их использования.
Библиогр. 8 назв.