{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:57Z","timestamp":1753889817443,"version":"3.41.2"},"reference-count":17,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,3,2]],"date-time":"2012-03-02T00:00:00Z","timestamp":1330646400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["233599"],"award-info":[{"award-number":["233599"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>It is shown that the finite satisfiability problem for two-variable logic over structures with one total preorder relation, its induced successor relation, one linear order relation and some further unary relations is EXPSPACE-complete. Actually, EXPSPACE-completeness already holds for structures that do not include the induced successor relation. As a special case, the EXPSPACE upper bound applies to two-variable logic over structures with two linear orders. A further consequence is that satisfiability of two-variable logic over data words with a linear order on positions and a linear order and successor relation on the data is decidable in EXPSPACE. As a complementing result, it is shown that over structures with two total preorder relations as well as over structures with one total preorder and two linear order relations, the finite satisfiability problem for two-variable logic is undecidable.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:15)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":7,"title":["Two-Variable Logic with Two Order Relations"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Thomas","family":"Schwentick","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Zeume","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,3,2]]},"reference":[{"key":"10.2168\/LMCS-8(1:15)2012_BojanczykMuscholl+Two-Variable06","doi-asserted-by":"crossref","unstructured":"Mikolaj Bojanczyk, Anca Muscholl, Thomas Schwentick, Luc Segoufin, and Claire David,Two-variable logic on words with data, LICS, 2006, pp. 7-16.","DOI":"10.1109\/LICS.2006.51"},{"key":"10.2168\/LMCS-8(1:15)2012_Boas1997","doi-asserted-by":"crossref","unstructured":"Peter Van Emde Boas,The convenience of tilings, In Complexity, Logic, and Recursion Theory, Marcel Dekker Inc, 1997, pp. 331-363.","DOI":"10.1201\/9780429187490-12"},{"key":"10.2168\/LMCS-8(1:15)2012_CohnHazarikaQualitative01","unstructured":"Anthony G. Cohn and Shyamanta M. Hazarika,Qualitative spatial representation and reasoning: An overview, Fundam. Inform. 46 (2001), no. 1-2, 1-29."},{"key":"10.2168\/LMCS-8(1:15)2012_DemriLazicLTL09","unstructured":"St\u00e9phane Demri and Ranko Lazic,LTLwith the freeze quantifier and register automata, ACM Trans. Comput. Log. 10 (2009), no. 3, 16:1-16:30."},{"key":"10.2168\/LMCS-8(1:15)2012_FigueiraSegoufinFuture-Looking09","doi-asserted-by":"crossref","unstructured":"Diego Figueira and Luc Segoufin,Future-looking logics on data words and trees, MFCS, 2009, pp. 331-343.","DOI":"10.1007\/978-3-642-03816-7_29"},{"key":"10.2168\/LMCS-8(1:15)2012_GradelKV97","unstructured":"Erich Gr\u00e4del, Phokion G. Kolaitis, and Moshe Y. Vardi,On the decision problem for two-variable first-order logic, Bulletin of Symbolic Logic 3 (1997), no. 1, 53-69."},{"key":"10.2168\/LMCS-8(1:15)2012_GraedelO1999","unstructured":"Erich Gr\u00e4del and Martin Otto,On logics with two variables, Theor. Comput. Sci.224 (1999), no. 1-2, 73-113."},{"key":"10.2168\/LMCS-8(1:15)2012_KieronskiOttoSmall05","doi-asserted-by":"crossref","unstructured":"Emanuel Kieronski and Martin Otto,Small substructures and decidability issues for first-order logic with two variables, LICS, 2005, pp. 448-457.","DOI":"10.1109\/LICS.2005.49"},{"key":"10.2168\/LMCS-8(1:15)2012_KieronskiTenderaOn09","doi-asserted-by":"crossref","unstructured":"Emanuel Kieronski and Lidia Tendera,On finite satisfiability of two-variable first-order logic with equivalence relations, LICS, 2009, pp. 123-132.","DOI":"10.1109\/LICS.2009.39"},{"key":"10.2168\/LMCS-8(1:15)2012_Manuel10","doi-asserted-by":"crossref","unstructured":"Amaldev Manuel,Two variables and two successors, MFCS, 2010, pp. 513-524.","DOI":"10.1007\/978-3-642-15155-2_45"},{"key":"10.2168\/LMCS-8(1:15)2012_MortimerOn75","doi-asserted-by":"crossref","unstructured":"M. Mortimer,On languages with two variables, Zeitschr. f. math. Logik u. Grundlagen d. Math. 21 (1975), 135-140.","DOI":"10.1002\/malq.19750210118"},{"key":"10.2168\/LMCS-8(1:15)2012_MarxR1997","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/9.6.897"},{"key":"10.2168\/LMCS-8(1:15)2012_ManuelZ11","unstructured":"Amaldev Manuel and Thomas Zeume,Personal communication., 2011."},{"key":"10.2168\/LMCS-8(1:15)2012_OttoTwo01","unstructured":"Martin Otto,Two variable first-order logic over ordered domains, J. Symb. Log. 66 (2001), no. 2, 685-702."},{"key":"10.2168\/LMCS-8(1:15)2012_SegoufinAutomata06","doi-asserted-by":"crossref","unstructured":"Luc Segoufin,Automata and logics for words and trees over an infinite alphabet, CSL, 2006, pp. 41-57.","DOI":"10.1007\/11874683_3"},{"key":"10.2168\/LMCS-8(1:15)2012_SchwentickZ10","doi-asserted-by":"crossref","unstructured":"Thomas Schwentick and Thomas Zeume,Two-variable logic with two order relations - (extended abstract), CSL, 2010, pp. 499-513.","DOI":"10.1007\/978-3-642-15205-4_38"},{"key":"10.2168\/LMCS-8(1:15)2012_Venema1990","unstructured":"Yde Venema,Expressiveness and completeness of an interval tense logic, Notre Dame Journal of Formal Logic 31 (1990), no. 4, 529-547."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/715\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/715\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T23:10:16Z","timestamp":1744067416000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/715"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,2]]},"references-count":17,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:15)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1110.1439","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1110.1439","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1145\/2724711","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,3,2]]},"article-number":"715"}}