Об алгоритмической сложности замкнутого фрагмента логики доказуемости GLP

В докладе будут рассмотрены задачи распознавания выводимости в полимодальной логике доказуемости GLP для некоторых классов формул. Основным результатом является доказательство PSPACE-полноты указанной задачи для формул без пропозициональных переменных. Также установлено, что при каждом фиксированном $n$ задача рассматриваемого вида для формул без пропозициональных переменных, содержащих не более, чем $n$ различных модальных связок, решается за полиномиальное время.