Модальная логика, аксиоматизированная с глубиной вложения, которая вряд ли будет в PSPACE?

Я ищу модальные логики, которые аксиоматизируются конечным набором аксиом глубины модальной вложенности, и чья проблема выполнимости / выводимости вряд ли будет в PSPACE. Без ограничения глубины модального вложения это не проблема, см., Например, PDL. Но, по-видимому, при доказательстве, например, EXPTIME-твердости путем снижения до некоторой проблемы плиточности или проблемы приемлемости для машин Тьюринга, потребуется некоторая транзитивность, которая аксиоматизирована на второй глубине. Существуют также неразрешимые логики с бинарной модальностью (Kurucz et al .: Решаемые и неразрешимые логики с бинарной модальностью , 1995), но они обычно требуют ассоциативности, что также составляет глубину два. В условной логике, опять же, кажется, что нам нужна глубина два для EXPTIME-твердости (Фридман, Халперн:О сложности условной логики , 1994).

Можем ли мы получить EXPTIME-твердость с аксиомами глубины вложения один?

Справочная информация: Мы пытаемся найти общие процедуры принятия решений высокой сложности для логики, аксиоматизированной с глубиной вложения один.

$!A$$!A \multimap !!A$

(Я получил это далеко сразу, а затем я застрял - вот почему этот ответ так поздно.)

Тем не менее, я просто понял , что в неявной сложности, люди изменить экспоненциальный линейной логики более точно контролировать пространство и время использования выреза ликвидации. Критически, все системы для этого устраняют аксиому дублирования! В результате вы можете выбрать систему, для которой нормализация, вероятно, пройдет мимо PSPACE (например, элементарная аффинная логика столь же сильна, как элементарные ограниченные машины Тьюринга), и тогда аксиоматизация этого вряд ли будет в PSPACE, поскольку это подразумевает что вы можете быстро найти доказательства без сокращений.$!A$

Ссылка: Уго дал Лаго и Симона Мартини, Фазовая семантика и разрешимость элементарной аффинной логики

Я бы предложил почитать книгу Блэкберна, де Рийке и Венемы « Модальная логика» .