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

Первая часть доклада будет основана на статье: M. Y. Vardi, "On the complexity of epistemic reasoning," [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, 1989, pp. 243-252, doi: 10.1109/LICS.1989.39179.
Минимальную нормальную модальную логику K можно альтернативным образом аксиоматизировать, взяв в качестве правил Modus Ponens и правило E: $A\leftrightarrow B / \Box A \leftrightarrow \Box B$, а в качестве аксиом все тавтологии, (AN) $\Box \top$, (AM) $\Box (p \land q) \to \Box p$ и (AC) $\Box p \land \Box q \to \Box(p \land q)$. При этом Варди рассматривает различные подмножества этих аксиом и получает различные ненормальные модальные системы. Хорошо известно, что логика K является PSPACE полной (Ladner'1977).
В своей статье Варди, основываясь на окрестностной семантике, доказывает, что из всех логик, которые можно получить выбрав некоторые из перечисленных аксиом, логика является coNP-полной, если и только если она не содержит аксиому (AC). А если логика содержит аксиому (AC), то тем же способом удается доказать PSPACE, при этом доказательство для K оказывается проще, чем другие известные доказательства. Таким образом, в некотором смысле, основной вклад в сложность дает аксиома (AC). В первой части доклада я изложу этот метод.
Во второй части я определю логику с несколькими модальностями, которая в некотором смысле следит за количеством применения аксиомы (AC). Для этого мы рассмотрим язык с несколькими модальностями, по каждой модальности мы возьмем все аксиомы кроме (AC), а вместо аксиомы (AC) мы возьмем аксиомы вида $\Box_n p \land \Box_n q \to \Box_{n+1}(p \land q).$ Мы докажем, что такая логика в языке с конечным числом модальностей является coNP-полной.
Полная логика с бесконечным числом модальностей лежит в классе PSPACE. Можно интуитивно рассматривать такую систему, как эпистемическую логику агента, для которого применения всех аксиом, кроме (AC) является бесплатными, а за применением аксиомы (AC) он следит. При этом формула $\Box_n A$ понимается, как "агент знает, что $A$ верно, но чтобы это проверить ему нужно применить аксиому (AC) не более $n$ раз и сколько угодно раз остальные аксиомы и правила".