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

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

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