{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:12:33Z","timestamp":1750306353617,"version":"3.41.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2016,11,3]],"date-time":"2016-11-03T00:00:00Z","timestamp":1478131200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Polish NCN","award":["2011\/03\/B\/ST6\/00346"],"award-info":[{"award-number":["2011\/03\/B\/ST6\/00346"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2016,11,15]]},"abstract":"<jats:p>\n            We consider the two-variable logic with counting quantifiers (C\n            <jats:sup>2<\/jats:sup>\n            ) interpreted over finite structures that contain two forests of ranked trees. This logic is strictly more expressive than standard C\n            <jats:sup>2<\/jats:sup>\n            and it is no longer a fragment of first-order logic. In particular, it can express that a structure is a ranked tree, a cycle, or a connected graph of bounded degree. It is also strictly more expressive than first-order logic with two variables and two successor relations of two finite linear orders. We present a decision procedure for the satisfiability problem for this logic. The procedure runs in NE\n            <jats:sc>xp<\/jats:sc>\n            T\n            <jats:sc>ime<\/jats:sc>\n            , which is optimal since the satisfiability problem for plain C\n            <jats:sup>2<\/jats:sup>\n            is NE\n            <jats:sc>xp<\/jats:sc>\n            T\n            <jats:sc>ime<\/jats:sc>\n            -complete.\n          <\/jats:p>","DOI":"10.1145\/2983622","type":"journal-article","created":{"date-parts":[[2016,11,4]],"date-time":"2016-11-04T12:49:04Z","timestamp":1478263744000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Two-Variable Logic with Counting and Trees"],"prefix":"10.1145","volume":"17","author":[{"given":"Witold","family":"Charatonik","sequence":"first","affiliation":[{"name":"University of Wroc\u0142aw, Wroc\u0142aw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Witkowski","sequence":"additional","affiliation":[{"name":"University of Wroc\u0142aw, Wroc\u0142aw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,11,3]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_10"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516512.1516515"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.51"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_28"},{"key":"e_1_2_1_5_1","series-title":"Lecture Notes in Computer Science, Christian G","volume-title":"LPAR (Yogyakarta)","author":"Charatonik Witold","unstructured":"Witold Charatonik and Piotr Witkowski . 2010. On the complexity of the Bernays-Sch\u00f6nfinkel class with datalog . In LPAR (Yogyakarta) , Lecture Notes in Computer Science, Christian G . Ferm\u00fcller and Andrei Voronkov (Eds.), Vol. 6397 . Springer , Berlin , 187--201. Witold Charatonik and Piotr Witkowski. 2010. On the complexity of the Bernays-Sch\u00f6nfinkel class with datalog. In LPAR (Yogyakarta), Lecture Notes in Computer Science, Christian G. Ferm\u00fcller and Andrei Voronkov (Eds.), Vol. 6397. Springer, Berlin, 187--201."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.12"},{"key":"e_1_2_1_7_1","unstructured":"Witold Charatonik and Piotr Witkowski. 2016a. Bounded model checking of pointer programs revisited. CoRR abs\/1602.09061. http:\/\/arxiv.org\/abs\/1602.09061.  Witold Charatonik and Piotr Witkowski. 2016a. Bounded model checking of pointer programs revisited. CoRR abs\/1602.09061. http:\/\/arxiv.org\/abs\/1602.09061."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(2:8)2016"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.orl.2005.09.008"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2953"},{"key":"e_1_2_1_11_1","volume-title":"Satisfiability for two-variable logic with two successor relations on finite linear orders. Computing Research Repository abs\/1204.2495","author":"Figueira Diego","year":"2012","unstructured":"Diego Figueira . 2012. Satisfiability for two-variable logic with two successor relations on finite linear orders. Computing Research Repository abs\/1204.2495 ( 2012 ). http:\/\/arxiv.org\/abs\/1204.2495. Diego Figueira. 2012. Satisfiability for two-variable logic with two successor relations on finite linear orders. Computing Research Repository abs\/1204.2495 (2012). http:\/\/arxiv.org\/abs\/1204.2495."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.2307\/421196"},{"volume-title":"Two-variable logic with counting is decidable","author":"Gr\u00e4del Erich","key":"e_1_2_1_13_1","unstructured":"Erich Gr\u00e4del , Martin Otto , and Eric Rosen . 1997b. Two-variable logic with counting is decidable . In LICS. IEEE Computer Society , 306--317. Erich Gr\u00e4del, Martin Otto, and Eric Rosen. 1997b. Two-variable logic with counting is decidable. In LICS. IEEE Computer Society, 306--317."},{"key":"e_1_2_1_14_1","series-title":"Lecture Notes in Computer Science, R\u00fcdiger Reischuk and Michel Morvan (Eds.)","volume-title":"STACS","author":"Gr\u00e4del Erich","unstructured":"Erich Gr\u00e4del , Martin Otto , and Eric Rosen . 1997c. Undecidability results on two-variable logics . In STACS , Lecture Notes in Computer Science, R\u00fcdiger Reischuk and Michel Morvan (Eds.) , Vol. 1200 . Springer , Berlin , 249--260. Erich Gr\u00e4del, Martin Otto, and Eric Rosen. 1997c. Undecidability results on two-variable logics. In STACS, Lecture Notes in Computer Science, R\u00fcdiger Reischuk and Michel Morvan (Eds.), Vol. 1200. Springer, Berlin, 249--260."},{"key":"e_1_2_1_15_1","series-title":"Lecture Notes in Computer Science","volume-title":"14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201907), Yerevan, Armenia, October 15--19","author":"Kazakov Yevgeny","year":"2007","unstructured":"Yevgeny Kazakov , Ulrike Sattler , and Evgeny Zolin . 2007. How many legs do I have? Non-simple roles in number restrictions revisited . In 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201907), Yerevan, Armenia, October 15--19 , 2007 , Lecture Notes in Computer Science , Nachum Dershowitz and Andrei Voronkov (Eds.), Vol. 4790 . Springer , Berlin, 303--317. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-75560-9_23 10.1007\/978-3-540-75560-9_23 Yevgeny Kazakov, Ulrike Sattler, and Evgeny Zolin. 2007. How many legs do I have? Non-simple roles in number restrictions revisited. In 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201907), Yerevan, Armenia, October 15--19, 2007, Lecture Notes in Computer Science, Nachum Dershowitz and Andrei Voronkov (Eds.), Vol. 4790. Springer, Berlin, 303--317. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-75560-9_23"},{"key":"e_1_2_1_16_1","volume-title":"Marc Bezem (Ed.)","volume":"12","author":"Kiero\u0144ski Emanuel","year":"2011","unstructured":"Emanuel Kiero\u0144ski . 2011 . Decidability issues for two-variable logics with several linear orders. In CSL (LIPIcs) , Marc Bezem (Ed.) , Vol. 12 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 337--351. Emanuel Kiero\u0144ski. 2011. Decidability issues for two-variable logics with several linear orders. In CSL (LIPIcs), Marc Bezem (Ed.), Vol. 12. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 337--351."},{"key":"e_1_2_1_17_1","volume-title":"Patrick C\u00e9gielski and Arnaud Durand (Eds.)","volume":"16","author":"Kiero\u0144ski Emanuel","year":"2012","unstructured":"Emanuel Kiero\u0144ski and Jakub Michaliszyn . 2012 . Two-variable universal logic with transitive closure. In CSL (LIPIcs) , Patrick C\u00e9gielski and Arnaud Durand (Eds.) , Vol. 16 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 396--410. Emanuel Kiero\u0144ski and Jakub Michaliszyn. 2012. Two-variable universal logic with transitive closure. In CSL (LIPIcs), Patrick C\u00e9gielski and Arnaud Durand (Eds.), Vol. 16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 396--410."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.53"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.49"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.39"},{"volume-title":"Elements of Finite Model Theory","author":"Libkin Leonid","key":"e_1_2_1_21_1","unstructured":"Leonid Libkin . 2004. Elements of Finite Model Theory . Springer . Leonid Libkin. 2004. Elements of Finite Model Theory. Springer."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1885577.1885622"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19750210118"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1973.11993273"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.2307\/2695037"},{"volume-title":"Complexity of two-variable logic with counting","author":"Pacholski Leszek","key":"e_1_2_1_26_1","unstructured":"Leszek Pacholski , Wieslaw Szwast , and Lidia Tendera . 1997. Complexity of two-variable logic with counting . In LICS. IEEE , 318--327. Leszek Pacholski, Wieslaw Szwast, and Lidia Tendera. 1997. Complexity of two-variable logic with counting. In LICS. IEEE, 318--327."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10849-005-5791-1"},{"key":"e_1_2_1_28_1","series-title":"Lecture Notes in Computer Science, Anuj Dawar and Ruy J","volume-title":"WoLLIC","author":"Pratt-Hartmann Ian","unstructured":"Ian Pratt-Hartmann . 2010. The two-variable fragment with counting revisited . In WoLLIC , Lecture Notes in Computer Science, Anuj Dawar and Ruy J . G. B. de Queiroz (Eds.), Vol. 6188 . Springer , Berlin , 42--54. Ian Pratt-Hartmann. 2010. The two-variable fragment with counting revisited. In WoLLIC, Lecture Notes in Computer Science, Anuj Dawar and Ruy J. G. B. de Queiroz (Eds.), Vol. 6188. Springer, Berlin, 42--54."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603117"},{"volume-title":"CSL, Lecture Notes in Computer Science","author":"Schwentick Thomas","key":"e_1_2_1_30_1","unstructured":"Thomas Schwentick and Thomas Zeume . 2010. Two-variable logic with two order relations (extended abstract) . In CSL, Lecture Notes in Computer Science , Anuj Dawar and Helmut Veith (Eds.), Vol. 6247 . Springer , Berlin , 499--513. Thomas Schwentick and Thomas Zeume. 2010. Two-variable logic with two order relations (extended abstract). In CSL, Lecture Notes in Computer Science, Anuj Dawar and Helmut Veith (Eds.), Vol. 6247. Springer, Berlin, 499--513."},{"key":"e_1_2_1_31_1","first-page":"477","article-title":"A decision method for validity of sentences in two variables","volume":"27","author":"Scott Dana","year":"1962","unstructured":"Dana Scott . 1962 . A decision method for validity of sentences in two variables . Journal of Symbolic Logic 27 , 477 . Dana Scott. 1962. A decision method for validity of sentences in two variables. Journal of Symbolic Logic 27, 477.","journal-title":"Journal of Symbolic Logic"},{"key":"e_1_2_1_32_1","volume-title":"30th International Symposium on Theoretical Aspects of Computer Science (STACS\u201913)","volume":"20","author":"Szwast Wieslaw","year":"2013","unstructured":"Wieslaw Szwast and Lidia Tendera . 2013 . FO2 with one transitive relation is decidable . In 30th International Symposium on Theoretical Aspects of Computer Science (STACS\u201913) (Leibniz International Proceedings in Informatics (LIPIcs)) , Vol. 20 . Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 317--328. DOI:http:\/\/dx.doi.org\/10.4230\/LIPIcs.STACS.2013.317 10.4230\/LIPIcs.STACS.2013.317 Wieslaw Szwast and Lidia Tendera. 2013. FO2 with one transitive relation is decidable. In 30th International Symposium on Theoretical Aspects of Computer Science (STACS\u201913) (Leibniz International Proceedings in Informatics (LIPIcs)), Vol. 20. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 317--328. DOI:http:\/\/dx.doi.org\/10.4230\/LIPIcs.STACS.2013.317"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31856-9_7"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2983622","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2983622","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:56:02Z","timestamp":1750222562000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2983622"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,3]]},"references-count":33,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,11,15]]}},"alternative-id":["10.1145\/2983622"],"URL":"https:\/\/doi.org\/10.1145\/2983622","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2016,11,3]]},"assertion":[{"value":"2016-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-11-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}