{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:41:45Z","timestamp":1740134505823,"version":"3.37.3"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,3,6]],"date-time":"2014-03-06T00:00:00Z","timestamp":1394064000000},"content-version":"vor","delay-in-days":33,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Spanish Project FORMALISM"},{"DOI":"10.13039\/501100003086","name":"Eusko Jaurlaritza","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003086","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003451","name":"Euskal Herriko Unibertsitatea","doi-asserted-by":"publisher","award":["UFI11\/45"],"id":[{"id":"10.13039\/501100003451","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2014,2]]},"abstract":"We systematically investigate the complexity of model checking the existential positive fragment of first-order logic. In particular, for a set of existential positive sentences, we consider model checking where the sentence is restricted to fall into the set; a natural question is then to classify which sentence sets are tractable and which are intractable. With respect to fixed-parameter tractability, we give a general theorem that reduces this classification question to the corresponding question for primitive positive logic, for a variety of representations of structures. This general theorem allows us to deduce that an existential positive sentence set having bounded arity is fixed-parameter tractable if and only if each sentence is equivalent to one in bounded-variable logic. We then use the lens of classical complexity to study these fixed-parameter tractable sentence sets. We show that such a set can be NP-complete, and consider the length needed by a translation from sentences in such a set to bounded-variable logic; we prove superpolynomial lower bounds on this length using the theory of compilability, obtaining an interesting type of formula size lower bound. Overall, the tools, concepts, and results of this article set the stage for the future consideration of the complexity of model checking on more expressive logics.<\/jats:p>","DOI":"10.1145\/2559946","type":"journal-article","created":{"date-parts":[[2014,3,4]],"date-time":"2014-03-04T13:24:59Z","timestamp":1393939499000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["On the complexity of existential positive queries"],"prefix":"10.1145","volume":"15","author":[{"given":"Hubie","family":"Chen","sequence":"first","affiliation":[{"name":"Universidad del Pa\u00eds Vasco and IKERBASQUE, Basque Foundation for Science, Bilbao, Spain"}]}],"member":"320","published-online":{"date-parts":[[2014,3,6]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"S. Abiteboul R. Hull and V. Vianu. 1995. Foundations of Databases. Addison-Wesley. S. Abiteboul R. Hull and V. Vianu. 1995. Foundations of Databases. Addison-Wesley."},{"key":"e_1_2_1_2_1","first-page":"1","article-title":"Tree-width for first order formulae","volume":"8","author":"Adler Isolde","year":"2012","unstructured":"Isolde Adler and Mark Weyer . 2012 . Tree-width for first order formulae . Logic. Methods Comput. Sci. 8 , 1 . Isolde Adler and Mark Weyer. 2012. Tree-width for first order formulae. Logic. Methods Comput. Sci. 8, 1.","journal-title":"Logic. Methods Comput. Sci."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/772062.772064"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1131342.1131344"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3043"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/800105.803397"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.31"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2010.04.003"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming (CP'02)","volume":"2470","author":"Dalmau Victor","unstructured":"Victor Dalmau , Phokion G. Kolaitis , and Moshe Y. Vardi . 2002. Constraint satisfaction, bounded treewidth, and finite-variable logics . In Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming (CP'02) . Lecture Notes in Computer Science , vol. 2470 , Springer-Verlag, Berlin, 310--326. Victor Dalmau, Phokion G. Kolaitis, and Moshe Y. Vardi. 2002. Constraint satisfaction, bounded treewidth, and finite-variable logics. In Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming (CP'02). Lecture Notes in Computer Science, vol. 2470, Springer-Verlag, Berlin, 310--326."},{"volume-title":"Finite Model Theory","author":"Ebbinghaus Heinz-Dieter","key":"e_1_2_1_10_1","unstructured":"Heinz-Dieter Ebbinghaus and J\u00f6rg Flum . 1995. Finite Model Theory . Springer . Heinz-Dieter Ebbinghaus and J\u00f6rg Flum. 1995. Finite Model Theory. Springer."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/602220.602222"},{"key":"e_1_2_1_12_1","unstructured":"J. Flum and M. Grohe. 2006. Parameterized Complexity Theory. Springer. J. Flum and M. Grohe. 2006. Parameterized Complexity Theory. Springer."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1206035.1206036"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(1:6)2005"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/380752.380867"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(92)90282-K"},{"key":"e_1_2_1_17_1","first-page":"191","article-title":"Turing machines that take advice","volume":"28","author":"Karp R. M.","year":"1982","unstructured":"R. M. Karp and R. J. Lipton . 1982 . Turing machines that take advice . L'Enseignement Math\u00e9matique 28 , 191 -- 209 . R. M. Karp and R. J. Lipton. 1982. Turing machines that take advice. L'Enseignement Math\u00e9matique 28, 191--209.","journal-title":"L'Enseignement Math\u00e9matique"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1713"},{"key":"e_1_2_1_19_1","volume-title":"Madelaine and Barnaby Martin","author":"Florent","year":"2012","unstructured":"Florent R. Madelaine and Barnaby Martin . 2012 . On the complexity of the model checking problem. CoRR abs\/1210.6893. Florent R. Madelaine and Barnaby Martin. 2012. On the complexity of the model checking problem. CoRR abs\/1210.6893."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806689.1806790"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806689.1806790"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-009-9248-9"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1379759.1379763"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/212433.212474"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2559946","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T18:37:42Z","timestamp":1672425462000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2559946"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["10.1145\/2559946"],"URL":"https:\/\/doi.org\/10.1145\/2559946","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2014,2]]},"assertion":[{"value":"2012-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-03-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}