{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:10Z","timestamp":1753889770237,"version":"3.41.2"},"reference-count":29,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,3,29]],"date-time":"2012-03-29T00:00:00Z","timestamp":1332979200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We introduce tree-width for first order formulae \\phi, fotw(\\phi). We show\nthat computing fotw is fixed-parameter tractable with parameter fotw. Moreover,\nwe show that on classes of formulae of bounded fotw, model checking is fixed\nparameter tractable, with parameter the length of the formula. This is done by\ntranslating a formula \\phi\\ with fotw(\\phi)&lt;k into a formula of the k-variable\nfragment L^k of first order logic. For fixed k, the question whether a given\nfirst order formula is equivalent to an L^k formula is undecidable. In\ncontrast, the classes of first order formulae with bounded fotw are fragments\nof first order logic for which the equivalence is decidable.\n  Our notion of tree-width generalises tree-width of conjunctive queries to\narbitrary formulae of first order logic by taking into account the quantifier\ninteraction in a formula. Moreover, it is more powerful than the notion of\nelimination-width of quantified constraint formulae, defined by Chen and Dalmau\n(CSL 2005): for quantified constraint formulae, both bounded elimination-width\nand bounded fotw allow for model checking in polynomial time. We prove that\nfotw of a quantified constraint formula \\phi\\ is bounded by the\nelimination-width of \\phi, and we exhibit a class of quantified constraint\nformulae with bounded fotw, that has unbounded elimination-width. A similar\ncomparison holds for strict tree-width of non-recursive stratified datalog as\ndefined by Flum, Frick, and Grohe (JACM 49, 2002).\n  Finally, we show that fotw has a characterization in terms of a cops and\nrobbers game without monotonicity cost.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:32)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":1,"title":["Tree-width for first order formulae"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Isolde","family":"Adler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Weyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2012,3,29]]},"reference":[{"key":"10.2168\/LMCS-8(1:32)2012_adl04","doi-asserted-by":"publisher","DOI":"10.1002\/jgt.20025"},{"key":"10.2168\/LMCS-8(1:32)2012_Adler07","doi-asserted-by":"publisher","DOI":"10.1016\/j.jctb.2006.12.006"},{"key":"10.2168\/LMCS-8(1:32)2012_Adler08a","doi-asserted-by":"publisher","DOI":"10.1137\/050623395"},{"key":"10.2168\/LMCS-8(1:32)2012_Adler08","doi-asserted-by":"publisher","DOI":"10.1145\/1376916.1376959"},{"issue":"1","key":"10.2168\/LMCS-8(1:32)2012_Arnborg85","first-page":"2","volume":"25","author":"Stefan Arnborg","year":"1985","journal-title":"BIT"},{"key":"10.2168\/LMCS-8(1:32)2012_Bodlaender96","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539793251219"},{"key":"10.2168\/LMCS-8(1:32)2012_chamer77","doi-asserted-by":"crossref","unstructured":"Ashok K. Chandra and Philip M. Merlin. Optimal implementation of conjunctive queries in relational data bases. InSTOC, pages 77-90. ACM, 1977.","DOI":"10.1145\/800105.803397"},{"key":"10.2168\/LMCS-8(1:32)2012_cheraj00","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00220-0"},{"key":"10.2168\/LMCS-8(1:32)2012_chedal05","doi-asserted-by":"crossref","unstructured":"Hubie Chen and V\u00edctor Dalmau. From pebble games to tractability: An ambidextrous consistency algorithm for quantified constraint satisfaction. In C.-H. Luke Ong, editor,CSL, volume 3634 ofLecture Notes in Computer Science, pages 232-247. Springer, 2005.","DOI":"10.1007\/11538363_17"},{"key":"10.2168\/LMCS-8(1:32)2012_dalkolvar02","doi-asserted-by":"crossref","unstructured":"V\u00edctor Dalmau, Phokion G. Kolaitis, and Moshe Y. Vardi. Constraint satisfaction, bounded treewidth, and finite-variable logics. In Pascal Van Hentenryck, editor,CP, volume 2470 ofLecture Notes in Computer Science, pages 310-326. Springer, 2002.","DOI":"10.1007\/3-540-46135-3_21"},{"key":"10.2168\/LMCS-8(1:32)2012_die06","doi-asserted-by":"crossref","unstructured":"Reinhard Diestel.Graph theory. Springer, Berlin, 2006.","DOI":"10.1007\/978-3-642-14279-6_7"},{"key":"10.2168\/LMCS-8(1:32)2012_DFT1996","unstructured":"Rod G. Downey, Michael R. Fellows, and Udayan Taylor. The parameterized complexity of relational database queries and an improved characterization of W[1]. In D. S. Bridges, C. Calude, P. Gibbons, S. Reeves, and I. H. Witten, editors,Combinatorics, Complexity, and Logic \u00e2\u0080\u0093 Proceedings of DMTCS \u00e2\u0080\u009996, pages 194-213. Springer-Verlag, 1996."},{"key":"10.2168\/LMCS-8(1:32)2012_DF99","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0515-9"},{"key":"10.2168\/LMCS-8(1:32)2012_ebbflu90","unstructured":"Heinz-Dieter Ebbinghaus and J\u00f6rg Flum.Finite Model Theory. Springer, 1990."},{"key":"10.2168\/LMCS-8(1:32)2012_fedvar98","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794266766"},{"key":"10.2168\/LMCS-8(1:32)2012_flufrigro01","doi-asserted-by":"publisher","DOI":"10.1145\/602220.602222"},{"key":"10.2168\/LMCS-8(1:32)2012_FG06","unstructured":"J\u00f6rg Flum and Martin Grohe.Parameterized Complexity Theory (Texts in Theoretical Computer Science. An EATCS Series). Springer-Verlag New York, Secaucus, NJ, USA, 2006."},{"key":"10.2168\/LMCS-8(1:32)2012_fre90","unstructured":"Eugene C. Freuder. Complexity of k-tree structured constraint satisfaction problems. InAAAI, pages 4-9, 1990."},{"key":"10.2168\/LMCS-8(1:32)2012_GottlobGS05","unstructured":"Georg Gottlob, Gianluigi Greco, and Francesco Scarcello. The complexity of quantified constraint satisfaction problems under structural restrictions. In Leslie Pack Kaelbling and Alessandro Saffiotti, editors,IJCAI, pages 150-155. Professional Book Center, 2005."},{"key":"10.2168\/LMCS-8(1:32)2012_gotleosca02","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2001.1809"},{"key":"10.2168\/LMCS-8(1:32)2012_gotleosca03","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(03)00030-8"},{"key":"10.2168\/LMCS-8(1:32)2012_Grohe07","doi-asserted-by":"publisher","DOI":"10.1145\/1206035.1206036"},{"key":"10.2168\/LMCS-8(1:32)2012_gromar06","doi-asserted-by":"crossref","unstructured":"Martin Grohe and D\u00e1niel Marx. Constraint solving via fractional edge covers. InSODA, pages 289-298. ACM Press, 2006.","DOI":"10.1145\/1109557.1109590"},{"key":"10.2168\/LMCS-8(1:32)2012_GroheSS01","doi-asserted-by":"crossref","unstructured":"Martin Grohe, Thomas Schwentick, and Luc Segoufin. When is the evaluation of conjunctive queries tractable? InSTOC, pages 657-666, 2001.","DOI":"10.1145\/380752.380867"},{"key":"10.2168\/LMCS-8(1:32)2012_KolaitisV00","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1713"},{"key":"10.2168\/LMCS-8(1:32)2012_kreord08","doi-asserted-by":"crossref","unstructured":"Stephan Kreutzer and Sebastian Ordyniak. Digraph decompositions and monotonicity in digraph searching. In Hajo Broersma, Thomas Erlebach, Tom Friedetzky, and Dani\u00ebl Paulusma, editors,WG, volume 5344 ofLecture Notes in Computer Science, pages 336-347, 2008.","DOI":"10.1007\/978-3-540-92248-3_30"},{"key":"10.2168\/LMCS-8(1:32)2012_seytho93","doi-asserted-by":"publisher","DOI":"10.1006\/jctb.1993.1027"},{"key":"10.2168\/LMCS-8(1:32)2012_vardi95","doi-asserted-by":"publisher","DOI":"10.1145\/212433.212474"},{"key":"10.2168\/LMCS-8(1:32)2012_yan81","unstructured":"Mihalis Yannakakis. Algorithms for acyclic database schemes. InVLDB, pages 82-94. IEEE Computer Society, 1981."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/786\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/786\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:55:53Z","timestamp":1681242953000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/786"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,29]]},"references-count":29,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:32)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1203.3814","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1203.3814","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,3,29]]},"article-number":"786"}}