Доклад Михаила Рыбакова и Дмитрия Шкатова на конференции «Автоматический вывод в количественных неклассических логиках» (Лиссабон, Португалия)

24 июля конференции в Лиссабоне Дмитрий Шкатов и Михаил Рыбаков представил доклад об алгоритмических свойствах модальных логик первого порядка для классов деревьев. 

24 июля 2026 года М. Рыбаковым и Д. Шкатовым был представлен доклад (докладчик Д. Шкатов) на конференции «Автоматический вывод в количественных неклассических логиках» (ARQNL 2026), проходившей в Лиссабоне, Португалия. Тема доклада — «Алгоритмические свойства модальных логик первого порядка некоторых классов деревьев». Известно, что классическая логика первого порядка алгоритмически неразрешима, но её монадический фрагмент (то есть фрагмент, в котором используются только унарные предикатные буквы) разрешим. Авторы показали, что результат о разрешимости монадического фрагмента остаётся верным для любой модальной предикатной логики, определяемой шкалой Крипке, являющейся конечным деревом, но для многих логик, определяемых естественными бесконечными классами деревьев, оказывается неразрешимым, а иногда даже неарифметичным в языке всего лишь с двумя унарными предикатными буквами и двумя предметными переменными. Это означает, в частности, что соответствующие логики (и даже их фрагменты в указанном языке) невозможно аксиоматизировать рекурсивно, и тем более с помощью конечного списка аксиом.