{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:45:38Z","timestamp":1762101938641,"version":"3.41.0"},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2016,11,11]],"date-time":"2016-11-11T00:00:00Z","timestamp":1478822400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Engineering and Physical Science Research Council projects \u201cEnforcement of Constraints on XML Streams\u201d","award":["EP\/G004021\/1"],"award-info":[{"award-number":["EP\/G004021\/1"]}]},{"DOI":"10.13039\/501100004281","name":"Polish National Science Centre","doi-asserted-by":"crossref","award":["DEC-2011\/03\/B\/ST6\/00346, DEC-2013\/09\/B\/ST6\/01535, DEC-2011\/03\/B\/ST6\/00346 and DEC-2013\/09\/N\/ST6\/01170"],"award-info":[{"award-number":["DEC-2011\/03\/B\/ST6\/00346, DEC-2013\/09\/B\/ST6\/01535, DEC-2011\/03\/B\/ST6\/00346 and DEC-2013\/09\/N\/ST6\/01170"]}],"id":[{"id":"10.13039\/501100004281","id-type":"DOI","asserted-by":"crossref"}]},{"name":"DBOnto: Bridging Ontologies and Databases","award":["EP\/L012138\/1"],"award-info":[{"award-number":["EP\/L012138\/1"]}]}],"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            Verification of properties expressed in the two-variable fragment of first-order logic FO\n            <jats:sup>2<\/jats:sup>\n            has been investigated in a number of contexts. The satisfiability problem for FO\n            <jats:sup>2<\/jats:sup>\n            over arbitrary structures is known to be NEXPTIME-complete, with satisfiable formulas having exponential-sized models. Over words, where FO\n            <jats:sup>2<\/jats:sup>\n            is known to have the same expressiveness as unary temporal logic, satisfiability is again NEXPTIME-complete. Over finite labelled ordered trees, FO\n            <jats:sup>2<\/jats:sup>\n            has the same expressiveness as navigational XPath, a popular query language for XML documents. Prior work on XPath and FO\n            <jats:sup>2<\/jats:sup>\n            gives a 2EXPTIME bound for satisfiability of FO\n            <jats:sup>2<\/jats:sup>\n            over trees. This work contains a comprehensive analysis of the complexity of FO\n            <jats:sup>2<\/jats:sup>\n            on trees, and on the size and depth of models. We show that different techniques are required depending on the vocabulary used, whether the trees are ranked or unranked, and the encoding of labels on trees. We also look at a natural restriction of FO\n            <jats:sup>2<\/jats:sup>\n            , its guarded version, \u2009GF\n            <jats:sup>2<\/jats:sup>\n            . Our results depend on an analysis of types in models of FO\n            <jats:sup>2<\/jats:sup>\n            formulas, including techniques for controlling the number of distinct subtrees, the depth, and the size of a witness to satisfiability for FO\n            <jats:sup>2<\/jats:sup>\n            sentences over finite trees.\n          <\/jats:p>","DOI":"10.1145\/2996796","type":"journal-article","created":{"date-parts":[[2016,11,11]],"date-time":"2016-11-11T17:02:54Z","timestamp":1478883774000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Complexity of Two-Variable Logic on Finite Trees"],"prefix":"10.1145","volume":"17","author":[{"given":"Saguy","family":"Benaim","sequence":"first","affiliation":[{"name":"University of Oxford, Parks Road, Oxford UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Benedikt","sequence":"additional","affiliation":[{"name":"University of Oxford, Parks Road, Oxford UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Witold","family":"Charatonik","sequence":"additional","affiliation":[{"name":"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"}]},{"given":"Rastislav","family":"Lenhardt","sequence":"additional","affiliation":[{"name":"University of Oxford"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Filip","family":"Mazowiecki","sequence":"additional","affiliation":[{"name":"University of Warsaw, Coventry, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Worrell","sequence":"additional","affiliation":[{"name":"University of Oxford, Parks Road, Oxford UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,11,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1004275029985"},{"key":"e_1_2_1_2_1","unstructured":"Saguy Benaim Michael Benedikt Rastislav Lenhardt and James Worrell. 2013. Controlling the depth size and number of subtrees in two variable logic over trees. CoRR abs\/1304.6925.  Saguy Benaim Michael Benedikt Rastislav Lenhardt and James Worrell. 2013. Controlling the depth size and number of subtrees in two variable logic over trees. CoRR abs\/1304.6925."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1346330.1346333"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1456650.1456653"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2012.38"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516512.1516515"},{"key":"e_1_2_1_7_1","unstructured":"Witold Charatonik Emanuel Kiero\u0144ski and Filip Mazowiecki. 2013. Satisfiability of the two-variable fragment of first-order logic over trees. CoRR abs\/1304.7204.  Witold Charatonik Emanuel Kiero\u0144ski and Filip Mazowiecki. 2013. Satisfiability of the two-variable fragment of first-order logic over trees. CoRR abs\/1304.7204."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603134"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.12"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2953"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362355.2362362"},{"key":"e_1_2_1_12_1","unstructured":"Diego Figueira. 2012b. Satisfiability for two-variable logic with two successor relations on finite linear orders. CoRR abs\/1204.2495.  Diego Figueira. 2012b. Satisfiability for two-variable logic with two successor relations on finite linear orders. CoRR abs\/1204.2495."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586808"},{"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":"crossref","unstructured":"Emanuel Kiero\u0144ski. 2002. EXPSPACE-complete variant of guarded fragment with transitivity. In STACS. 608--619.   Emanuel Kiero\u0144ski. 2002. EXPSPACE-complete variant of guarded fragment with transitivity. In STACS. 608--619.","DOI":"10.1007\/3-540-45841-7_50"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_22"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Maarten Marx. 2004. XPath with conditional axis relations. In EDBT. 477--494.  Maarten Marx. 2004. XPath with conditional axis relations. In EDBT. 477--494.","DOI":"10.1007\/978-3-540-24741-8_28"},{"key":"e_1_2_1_18_1","unstructured":"Maarten Marx and Maarten de Rijke. 2004. Semantic characterization of navigational XPath. In TDM. 73--79.  Maarten Marx and Maarten de Rijke. 2004. Semantic characterization of navigational XPath. In TDM. 73--79."},{"key":"e_1_2_1_19_1","first-page":"477","article-title":"A decision method for validity of sentences in two variables","volume":"27","author":"Scott Dana S.","year":"1962","unstructured":"Dana S. Scott . 1962 . A decision method for validity of sentences in two variables . Journal of Symbolic Logic 27 (1962), 477 . Dana S. Scott. 1962. A decision method for validity of sentences in two variables. Journal of Symbolic Logic 27 (1962), 477.","journal-title":"Journal of Symbolic Logic"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.01.003"},{"key":"e_1_2_1_22_1","volume-title":"STACS(LIPIcs)","volume":"20","author":"Szwast Wieslaw","year":"2013","unstructured":"Wieslaw Szwast and Lidia Tendera . 2013 . FO2 with one transitive relation is decidable . In STACS(LIPIcs) , Vol. 20 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 317--328. Wieslaw Szwast and Lidia Tendera. 2013. FO2 with one transitive relation is decidable. In STACS(LIPIcs), Vol. 20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 317--328."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2559945"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2996796","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2996796","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:49Z","timestamp":1750273549000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2996796"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,11]]},"references-count":22,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,11,15]]}},"alternative-id":["10.1145\/2996796"],"URL":"https:\/\/doi.org\/10.1145\/2996796","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2016,11,11]]},"assertion":[{"value":"2014-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-11-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}