engleski

Complexity of the interpretability logic IL

This talk is based on the paper [MPV18]. Computational complexity of modal logics was first studied by Ladner [Lad77]. Various tableau– based methods were used in proofs of PSPACE– decidability of a number of modal logics (like K, K4, S4 etc ; see [Lad77] and [Spa93]). PSPACE– completeness of the satisfiability problem (and also of the decision problem, since co-PSPACE = PSPACE) for the closed fragments of modal systems K4, S4, Grz and GL is proved by Chagrov and Rybakov [CR03]. Shapirovsky [Sha10] proved the PSPACE– decidability of propositional polymodal provability logic GLP. PSPACE–completeness of the closed fragment of the system GLP is proved by Pakhomov in [Pak14]. The interpretability logic IL, introduced by Visser [Vis90], is an extension of provability logic with a binary modal operator B. This operator stands for interpretability, considered as a relation between extensions of a fixed theory. Bou and Joosten proved in [BJ11] that the decidability problem for the closed fragment of IL is PSPACE–hard. We consider the complexity problem for interpretability logic and prove that the system IL is PSPACE–complete. Our constructions can be seen as generalizations of the constructions by Boolos presented in [Boo96] (Chapter 10). If we restrict our work to GL, the resulting method is very similiar to the one given by Boolos, up to the terminology. Our method can also be seen as extending the method presented in [Sha10], of proving PSPACE– completeness (monomodal case), and has similarities with the proofs od completeness in [GJ08] and [GJ11]. We will comment on extending this approach to other interpretability logics.

interpretability logic, Veltman semantics, decidability, complexity, PSPACE

nije evidentirano