PSpace-разрешимость модальных логик древовидных шкал

Доклад посвящён доказательству PSpace-разрешимости для широкого класса нормальных модальных логик. В основе метода лежит следующая идея: если формула совместна с логикой, то она выполнима в модели, имеющей древовидную структуру с полиномиальными ограничениями на высоту, ветвление и размер кластеров. При построении такой модели достаточно хранить в памяти лишь одну ветвь дерева, имеющую полиномиальный размер. Данная идея восходит к работам И. Б. Шапировского [1, 2], который развил её для транзитивных логик. Однако единая теорема, формулирующая условия на класс древовидных шкал, гарантирующие PSpace-разрешимость, ранее явно не была представлена. В докладе мы сформулируем и докажем такой общий результат.

Доклад планируется в двух частях. Сначала мы подробно разберём доказательство для базового случая, т.е. для логики K, введём ключевые понятия и сформулируем общие условия, гарантирующие PSpace-разрешимость. Затем мы докажем основную теорему и покажем, как она применяется к различным логикам: транзитивным (K4, S4, GL, S4.2), логике с симметричным отношением (KB), а также некоторым предтранзитивным и временным логикам.

От слушателей предполагается знакомство с основами семантики Крипке.