{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T12:36:44Z","timestamp":1775738204383,"version":"3.50.1"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,9,23]],"date-time":"2015-09-23T00:00:00Z","timestamp":1442966400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Austrian Science Fund (FWF)NFN","award":["S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award)"],"award-info":[{"award-number":["S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award)"]}]},{"name":"Polish National Science Center","award":["DEC-2011\/03\/N\/ST6\/00415"],"award-info":[{"award-number":["DEC-2011\/03\/N\/ST6\/00415"]}]},{"name":"Polish National Science Center","award":["DEC-2013\/09\/B\/ST6\/01535"],"award-info":[{"award-number":["DEC-2013\/09\/B\/ST6\/01535"]}]},{"name":"European Research Council","award":["267989 (QUAREM)"],"award-info":[{"award-number":["267989 (QUAREM)"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2015,12,10]]},"abstract":"<jats:p>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 either NP-complete or PS<jats:sc>pace<\/jats:sc>-complete, and global satisfiability is NP-complete, PS<jats:sc>pace<\/jats:sc>-complete, or E<jats:sc>xp<\/jats:sc>T<jats:sc>ime<\/jats:sc>-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.<\/jats:p>","DOI":"10.1145\/2817825","type":"journal-article","created":{"date-parts":[[2015,9,29]],"date-time":"2015-09-29T19:22:29Z","timestamp":1443554549000},"page":"1-47","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["On the Decidability of Elementary Modal Logics"],"prefix":"10.1145","volume":"17","author":[{"given":"Jakub","family":"Michaliszyn","sequence":"first","affiliation":[{"name":"Imperial College London and University of Wroc\u0142aw, Wroc\u0142aw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Otop","sequence":"additional","affiliation":[{"name":"IST Austria and University of Wroc\u0142aw, Wroc\u0142aw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emanuel","family":"Kiero\u0144ski","sequence":"additional","affiliation":[{"name":"University of Wroc\u0142aw, Wroc\u0142aw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,9,23]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP\u201911)","author":"B\u00e1r\u00e1ny Vince","year":"2011"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Robert Berger. 1966. The undecidability of the domino problem. Memmoirs of the American Mathematical Society 66. Robert Berger. 1966. The undecidability of the domino problem. Memmoirs of the American Mathematical Society 66.","DOI":"10.1090\/memo\/0066"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/381193"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586808"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/788019.788870"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00971620"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1040046086"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 25th Annual Symposium on Theoretical Aspects of Computer Science (STACS\u201908)","author":"Hemaspaandra Edith","year":"2008"},{"key":"e_1_2_1_9_1","volume-title":"MFCS (LNCS)","author":"Hemaspaandra Edith"},{"key":"e_1_2_1_10_1","volume-title":"FSTTCS (LIPIcs)","volume":"13","author":"Kiero\u0144ski Emanuel","year":"2011"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.53"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.49"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1137\/0206033"},{"key":"e_1_2_1_14_1","volume-title":"Advances in Modal Logic","author":"Michaliszyn Jakub"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.59"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19750210118"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.2307\/2695037"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Leszek Pacholski Wieslaw Szwast and Lidia Tendera. 1997. Complexity of two-variable logic with counting. In LICS. IEEE Computer Society Washington DC 318--327. Leszek Pacholski Wieslaw Szwast and Lidia Tendera. 1997. Complexity of two-variable logic with counting. In LICS. IEEE Computer Society Washington DC 318--327.","DOI":"10.1109\/LICS.1997.614958"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10849-005-5791-1"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70728-6"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(70)80006-X"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 30th International Symposium on Theoretical Aspects of Computer Science (STACS\u201913)","author":"Szwast Wieslaw","year":"2013"},{"key":"e_1_2_1_23_1","volume-title":"Complexity, Logic, and Recursion Theory","author":"van Emde Boas Peter"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2817825","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2817825","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:43:25Z","timestamp":1750225405000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2817825"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,23]]},"references-count":23,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,12,10]]}},"alternative-id":["10.1145\/2817825"],"URL":"https:\/\/doi.org\/10.1145\/2817825","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,23]]},"assertion":[{"value":"2013-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-09-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}