#матлог #учёба #спецсеминар

25 марта 2026 г. состоится заседание Рабочего семинара по математической логике под руководством С.Л. Кузнецова и С.О. Сперанского, в рамках НОЦ МИАН.

Время начала: 16:00
Место: МИАН (ул. Губкина, 8), ауд. 303 + Контур.Толк
Всех слушателей просим зарегистрироваться на странице семинара: www.mathnet.ru/conf2533

Н.В. Лукашов (НИУ ВШЭ)

Вычислительные аспекты для модальных логик

Аннотация:

Рассказ будет посвящён исследованию разрешимости и вычислительной сложности нормальных модальных логик. В первой части будут рассмотрены различные методы доказательства разрешимости для логик, обладающих свойством конечных моделей. Будет показано, что наличие этого свойства само по себе не гарантирует существование эффективных алгоритмов: будет приведена конструкция несчётного семейства даже полиномиально аппроксимируемых логик с неразрешимой проблемой принадлежности. Затем мы обсудим различные семантические и синтаксические ограничения, при наложении которых удаётся установить разрешимость в целом, без оценки требуемых вычислительных ресурсов.

Далее мы сосредоточимся на границах сложности. После краткого напоминания классов P, NP и PSPACE будет изложен общий метод установления NP-полноты для нормальных модальных логик и, в частности, продемонстрировано, что логика S5 является таковой. Затем будет приведена общая конструкция, показывающая, что такие модальные логики, как K, K4, S4 и GL, не являются полиномиально аппроксимируемыми, что будет означать необходимость принципиально иных подходов к установлению их принадлежности к PSPACE (об этом пойдёт речь в последующих докладах Л.В. Дворкина). В заключение, используя приведённую конструкцию для задачи TQBF, мы также воспроизведем доказательство классической теоремы Р. Ладнера (1979), утверждающей, что любая нормальная модальная логика в интервале между K и S4 является PSPACE-трудной.

Некоторая литература:

P. Blackburn, M. De Rijke, Y. Venema. Modal Logic. Cambridge University Press, 2001.
R.E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing 6(3), 467–480, 1977.