Аннотация:
Представлен критерий допустимости правил вывода с метапеременными в модальной логике $S4.\alpha_N$. Тем самым в логике $S4.\alpha_N$ решена проблема подстановки и получен алгоритм, распознающий разрешимость логических уравнений. Другим следствием критерия является разрешимость соответствующей квазиэквациональной теории свободной модальной алгебры в сигнатуре, обогащенной константами для свободных порождающих.
Ключевые слова:допустимое правило вывода, метапеременная, модальная логика, правило вывода.
Полный текст:
PDF файл (251 kB)
