Modal logics are widely used in computer science. The complexity of modal satisfiability problems has been investigated since the 1970s, usually proving results on a case-by-case basis. We prove a very general classification for a wide class of relevant logics: Many important subclasses of modal logics can be obtained by restricting the allowed models with first-order Horn formulas. We show that the satisfiability problem for each of these logics is either NP-complete or PSPACE-hard, and exhibit a simple classification criterion. Further, we prove matching PSPACE upper bounds for many of the PSPACE-hard logics.
@InProceedings{hemaspaandra_et_al:LIPIcs.STACS.2008.1356, author = {Hemaspaandra, Edith and Schnoor, Henning}, title = {{On the Complexity of Elementary Modal Logics}}, booktitle = {25th International Symposium on Theoretical Aspects of Computer Science}, pages = {349--360}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-06-4}, ISSN = {1868-8969}, year = {2008}, volume = {1}, editor = {Albers, Susanne and Weil, Pascal}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008.1356}, URN = {urn:nbn:de:0030-drops-13561}, doi = {10.4230/LIPIcs.STACS.2008.1356}, annote = {Keywords: } }
Feedback for Dagstuhl Publishing