{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T12:36:43Z","timestamp":1775738203053,"version":"3.50.1"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,3,1]],"date-time":"2015-03-01T00:00:00Z","timestamp":1425168000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DFG research project ProbDL"},{"name":"DFG research project GELO"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2015,3]]},"abstract":"<jats:p>\n            We study the satisfiability problem of the logic K\n            <jats:sup>2<\/jats:sup>\n            = K \u00d7 K\u2014the two-dimensional variant of unimodal logic, where models are restricted to asynchronous products of two Kripke frames. Gabbay and Shehtman proved in 1998 that this problem is decidable in a tower of exponentials. So far, the best-known lower bound is NEXP-hardness shown by Marx and Mikul\u00e1s in 2001.\n          <\/jats:p>\n          <jats:p>\n            Our first main result closes this complexity gap. We show that satisfiability in K\n            <jats:sup>2<\/jats:sup>\n            is nonelementary. More precisely, we prove that it is\n            <jats:italic>k<\/jats:italic>\n            -NEXP-complete, where\n            <jats:italic>k<\/jats:italic>\n            is the switching depth (the minimal modal rank among the two dimensions) of the input formula, hereby solving a conjecture of Marx and Mikul\u00e1s. Using our lower-bound technique also allows us to derive nonelementary lower bounds for the two-dimensional modal logics K4 \u00d7 K and S5\n            <jats:sub>2<\/jats:sub>\n            \u00d7 K, for which only elementary lower bounds were previously known.\n          <\/jats:p>\n          <jats:p>\n            Moreover, we apply our technique to prove nonelementary lower bounds for the sizes of Feferman-Vaught decompositions with respect to product for any decomposable logic that is at least as expressive as unimodal K, generalizing a recent result by the first author and Lin. For the three-variable fragment FO\n            <jats:sup>3<\/jats:sup>\n            of first-order logic, we obtain the following two immediate corollaries: the size of Feferman-Vaught decompositions with respect to disjoint sum are inherently nonelementary, and equivalent formulas in Gaifman normal form are inherently nonelementary.\n          <\/jats:p>\n          <jats:p>\n            Our second main result consists in providing effective elementary (more precisely, doubly exponential) upper bounds for the two-variable fragment FO\n            <jats:sup>2<\/jats:sup>\n            of first-order logic both for Feferman-Vaught decompositions and for equivalent formulas in Gaifman normal form.\n          <\/jats:p>","DOI":"10.1145\/2699918","type":"journal-article","created":{"date-parts":[[2015,3,25]],"date-time":"2015-03-25T16:03:43Z","timestamp":1427299423000},"page":"1-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["The Complexity of Decomposing Modal and First-Order Theories"],"prefix":"10.1145","volume":"16","author":[{"given":"Stefan","family":"G\u00f6ller","sequence":"first","affiliation":[{"name":"University of Bremen"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Christoph","family":"Jung","sequence":"additional","affiliation":[{"name":"University of Bremen, Postfach, Bremen"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Lohrey","sequence":"additional","affiliation":[{"name":"University of Leipzig"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,3,24]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"P. Blackburn M. de Rijke and Y. Venema. 2001. Modal Logic. Cambridge University Press.   P. Blackburn M. de Rijke and Y. Venema. 2001. Modal Logic. Cambridge University Press.","DOI":"10.1017\/CBO9781107050884"},{"key":"e_1_2_1_2_1","unstructured":"P. Blackburn F. Wolter and J. van Benthem (Eds.). 2006. Handbook of Modal Logic. Elsevier.  P. Blackburn F. Wolter and J. van Benthem (Eds.). 2006. Handbook of Modal Logic. Elsevier."},{"key":"e_1_2_1_3_1","unstructured":"E. B\u00f6rger E. Gr\u00e4del and Y. Gurevich. 2001. The Classical Decision Problem. Springer-Verlag Berlin Heidelberg.  E. B\u00f6rger E. Gr\u00e4del and Y. Gurevich. 2001. The Classical Decision Problem. Springer-Verlag Berlin Heidelberg."},{"key":"e_1_2_1_4_1","series-title":"Lecture Notes in Computer Science","volume-title":"Computation Theory","author":"Chlebus B. S.","unstructured":"B. S. Chlebus . 1984. From domino tilings to a new model of computation . In Computation Theory . Lecture Notes in Computer Science , Vol. 208 . Springer , 24--33. B. S. Chlebus. 1984. From domino tilings to a new model of computation. In Computation Theory. Lecture Notes in Computer Science, Vol. 208. Springer, 24--33."},{"key":"e_1_2_1_5_1","first-page":"913","article-title":"Model theory makes formulas large","volume":"4596","author":"Dawar A.","year":"2007","unstructured":"A. Dawar , M. Grohe , S. Kreutzer , and N. Schweikardt . 2007 . Model theory makes formulas large . In Automata, Languages and Programming. Lecture Notes in Computer Science , Vol. 4596. Spring er, 913 -- 924 . A. Dawar, M. Grohe, S. Kreutzer, and N. Schweikardt. 2007. Model theory makes formulas large. In Automata, Languages and Programming. Lecture Notes in Computer Science, Vol. 4596. Springer, 913--924.","journal-title":"Automata, Languages and Programming. Lecture Notes in Computer Science"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4064\/fm-47-1-57-103"},{"key":"e_1_2_1_7_1","unstructured":"J. Flum and M. Grohe. 2006. Parametrized Complexity Theory. Springer.   J. Flum and M. Grohe. 2006. Parametrized Complexity Theory. Springer."},{"key":"e_1_2_1_8_1","unstructured":"D. Gabbay A. Kurusz F. Wolter and M. Zakharyaschev. 2003. Many-Dimensional Modal Logics: Theory and Applications. Elsevier.  D. Gabbay A. Kurusz F. Wolter and M. Zakharyaschev. 2003. Many-Dimensional Modal Logics: Theory and Applications. Elsevier."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/6.1.73"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1122038925"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71879-2"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS\u201912)","author":"G\u00f6ller S.","unstructured":"S. G\u00f6ller and A. W. Lin . 2012. Concurrency makes simple theories hard . In Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS\u201912) . 344--355. S. G\u00f6ller and A. W. Lin. 2012. Concurrency makes simple theories hard. In Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS\u201912). 344--355."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.43"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.2307\/421196"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90039-1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1190150040"},{"key":"e_1_2_1_17_1","first-page":"147","article-title":"Algorithmic meta-theorems","volume":"16","author":"Kreutzer S.","year":"2009","unstructured":"S. Kreutzer . 2009 . Algorithmic meta-theorems . Electronic Colloquium on Computational Complexity 16 , 147 . S. Kreutzer. 2009. Algorithmic meta-theorems. Electronic Colloquium on Computational Complexity 16, 147.","journal-title":"Electronic Colloquium on Computational Complexity"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1137\/0206033"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2003.11.002"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/9.2.197"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/9.1.71"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"M. Marx and Y. Venema. 1996. Multi-Dimensional Modal Logic. Kluwer Academic Press.  M. Marx and Y. Venema. 1996. Multi-Dimensional Modal Logic. Kluwer Academic Press.","DOI":"10.1007\/978-94-011-5694-3"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.2307\/2267454"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1182613.1182617"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2699918","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2699918","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:59Z","timestamp":1750227419000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2699918"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,3]]}},"alternative-id":["10.1145\/2699918"],"URL":"https:\/\/doi.org\/10.1145\/2699918","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3]]},"assertion":[{"value":"2012-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-03-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}