On the decidability of elementary modal logics
Michaliszyn, Jakub
Otop, Jan
Kieroňski, Emanuel
We consider the satisfiability problem for modal logic over first-order definable classes of frames.We confirm the conjecture from Hemaspaandra and Schnoor [2008] that modal logic is decidable over classes definable by universal Horn formulae. We provide a full classification of Horn formulae with respect to the complexity of the corresponding satisfiability problem. It turns out, that except for the trivial case of inconsistent formulae, local satisfiability is eitherNP-complete or PSPACE-complete, and global satisfiability is NP-complete, PSPACE-complete, or ExpTime-complete. We also show that the finite satisfiability problem for modal logic over Horn definable classes of frames is decidable. On the negative side, we show undecidability of two related problems. First, we exhibit a simple universal three-variable formula defining the class of frames over which modal logic is undecidable. Second, we consider the satisfiability problem of bimodal logic over Horn definable classes of frames, and also present a formula leading to undecidability.
ACM
2015
info:eu-repo/semantics/article
doc-type:article
text
https://research-explorer.app.ist.ac.at/record/1680
Michaliszyn J, Otop J, Kieroňski E. On the decidability of elementary modal logics. <i>ACM Transactions on Computational Logic</i>. 2015;17(1). doi:<a href="https://doi.org/10.1145/2817825">10.1145/2817825</a>
eng
info:eu-repo/semantics/altIdentifier/doi/10.1145/2817825
info:eu-repo/grantAgreement/EC/FP7/267989
info:eu-repo/grantAgreement/FWF//S 11407_N23
info:eu-repo/grantAgreement/FWF//Z211
info:eu-repo/semantics/closedAccess