{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T13:23:40Z","timestamp":1770902620967,"version":"3.50.1"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"2","funder":[{"DOI":"10.13039\/501100000780","name":"European Union","doi-asserted-by":"crossref","award":["101071674"],"award-info":[{"award-number":["101071674"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]},{"name":"European Research Council","award":["771779, DeciGUT"],"award-info":[{"award-number":["771779, DeciGUT"]}]},{"name":"Federal Ministry of Research, Technology and Space, Germany"},{"name":"BMBF and DAAD","award":["57616814"],"award-info":[{"award-number":["57616814"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2026,4,30]]},"abstract":"\n We characterise the sentences in Monadic Second-Order Logic (MSO) that are over finite structures equivalent to a Datalog program, in terms of an existential pebble game. We also show that for every class\n \n \\({\\mathcal{C}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n of finite structures that can be expressed in MSO and is closed under homomorphisms, and for all\n \n \\(\\ell,k\\in{\\mathbb{N}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n , there exists a\n canonical<\/jats:italic>\n Datalog program\n \n \\(\\Pi\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n of width\n \n \\((\\ell,k)\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n in the sense of Feder and Vardi. The same characterisations also hold for Guarded Second-Order Logic (GSO), which properly extends MSO. To prove our results, we show that every class\n \n \\({\\mathcal{C}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n in GSO whose complement is closed under homomorphisms is a finite union of Constraint Satisfaction Problems (CSPs) of\n \n \\(\\omega\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n -categorical structures. The intersection of MSO and Datalog is known to contain the class of\n nested monadically defined queries (Nemodeq)<\/jats:italic>\n ; likewise, we show that the intersection of GSO and Datalog contains all problems that can be expressed by the more expressive language of\n \n nested guarded queries (GQ\n \n \\({}^{+}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n )\n <\/jats:italic>\n . Yet, by exploiting our results, we can show that neither of the two query languages can serve as a characterisation, as we exhibit a CSP whose complement corresponds to a query in the intersection of MSO and Datalog that is not expressible in GQ\n \n \\({}^{+}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n .\n <\/jats:p>","DOI":"10.1145\/3779418","type":"journal-article","created":{"date-parts":[[2025,12,12]],"date-time":"2025-12-12T03:00:40Z","timestamp":1765508440000},"page":"1-42","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Datalog-Expressibility for Monadic and Guarded Second-Order Logic"],"prefix":"10.1145","volume":"27","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8228-3611","authenticated-orcid":false,"given":"Manuel","family":"Bodirsky","sequence":"first","affiliation":[{"name":"Institut f\u00fcr Algebra, Fakult\u00e4t Mathematik, TU Dresden, Dresden, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-7421-8565","authenticated-orcid":false,"given":"Simon","family":"Kn\u00e4uer","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Algebra, Fakult\u00e4t Mathematik, TU Dresden, Dresden, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1609-2080","authenticated-orcid":false,"given":"Sebastian","family":"Rudolph","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Algebra, Fakult\u00e4t Mathematik, TU Dresden, Dresden, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,2,12]]},"reference":[{"key":"e_1_3_3_2_2","unstructured":"Serge Abiteboul Richard Hull and Victor Vianu. 1995. Foundations of Databases. Addison-Wesley. Retrieved from http:\/\/webdam.inria.fr\/Alice\/"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1004275029985"},{"issue":"18","key":"e_1_3_3_4_2","doi-asserted-by":"crossref","first-page":"1666","DOI":"10.1016\/j.tcs.2008.12.049","article-title":"Affine systems of equations and counting infinitary logic","volume":"410","author":"Atserias Albert","year":"2009","unstructured":"Albert Atserias, Andrei A. Bulatov, and Anuj Dawar. 2009. Affine systems of equations and counting infinitary logic. Theoretical Computer Science 410, 18 (2009), 1666\u20131683.","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_3_5_2","volume-title":"Proceedings of the 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201917)","volume":"68","author":"Barto Libor","year":"2017","unstructured":"Libor Barto, Michael Kompatscher, Miroslav Ol\u0161\u00e1k, Trung Van Pham, and Michael Pinsker. 2017. The equivalence of two dichotomy conjectures for infinite domain constraint satisfaction problems. In Proceedings of the 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201917), Article 68, 12 pages."},{"issue":"1","key":"e_1_3_3_6_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2556646","article-title":"Constraint satisfaction problems solvable by local consistency methods","volume":"61","author":"Barto Libor","year":"2014","unstructured":"Libor Barto and Marcin Kozik. 2014. Constraint satisfaction problems solvable by local consistency methods. Journal of the ACM 61, 1, Article 3 (2014), 1\u201319.","journal-title":"Journal of the ACM"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/2661643"},{"key":"e_1_3_3_8_2","unstructured":"Achim Blumensath. 2020. Monadic second-order logic. Lecture Notes."},{"key":"e_1_3_3_9_2","unstructured":"Achim Blumensath. 2025. Monadic Second-Order Model Theory. Lecture Notes. Retrieved from https:\/\/www.fi.muni.cz\/ blumens\/MSO2.pdf"},{"key":"e_1_3_3_10_2","unstructured":"Manuel Bodirsky. 2004. Constraint Satisfaction with Infinite Domains. Dissertation Humboldt-Universit\u00e4t zu Berlin."},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1017\/9781107337534"},{"issue":"2","key":"e_1_3_3_12_2","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1016\/j.tcs.2009.07.059","article-title":"Peek arc consistency","volume":"411","author":"Bodirsky Manuel","year":"2010","unstructured":"Manuel Bodirsky and Hubie Chen. 2010. Peek arc consistency. Theoretical Computer Science 411, 2 (2010), 445\u2013453.","journal-title":"Theoretical Computer Science"},{"issue":"8","key":"e_1_3_3_13_2","doi-asserted-by":"crossref","first-page":"3682","DOI":"10.1137\/080725209","article-title":"Quantified equality constraints","volume":"39","author":"Bodirsky Manuel","year":"2010","unstructured":"Manuel Bodirsky and Hubie Chen. 2010. Quantified equality constraints. SIAM Journal on Computing 39, 8 (2010), 3682\u20133699.","journal-title":"SIAM Journal on Computing"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1286198146"},{"key":"e_1_3_3_15_2","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/j.jcss.2012.05.012","article-title":"Datalog and constraint satisfaction with infinite templates","volume":"79","author":"Bodirsky Manuel","year":"2013","unstructured":"Manuel Bodirsky and V\u00edctor Dalmau. 2013. Datalog and constraint satisfaction with infinite templates. Journal on Computer and System Sciences 79 (2013), 79\u2013100.","journal-title":"Journal on Computer and System Sciences"},{"key":"e_1_3_3_16_2","first-page":"1","volume-title":"Proceedings of the Symposium on Logic in Computer Science (LICS)","author":"Bodirsky Manuel","year":"2021","unstructured":"Manuel Bodirsky, Thomas Feller, Simon Kn\u00e4uer, and Sebastian Rudolph. 2021. On logics and homomorphism closure. In Proceedings of the Symposium on Logic in Computer Science (LICS). IEEE, 1\u201313. Retrieved from https:\/\/arxiv.org\/abs\/2104.11955"},{"key":"e_1_3_3_17_2","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/978-3-540-70583-3_16","volume-title":"Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP)","author":"Bodirsky Manuel","year":"2008","unstructured":"Manuel Bodirsky and Martin Grohe. 2008. Non-dichotomies in constraint satisfaction complexity. In Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP). Luca Aceto, Ivan Damgard, Leslie Ann Goldberg, Magn\u00fas M. Halld\u00f3rsson, Anna Ing\u00f3lfsd\u00f3ttir, and Igor Walukiewicz (Eds.). Lecture Notes in Computer Science, Springer Verlag, 184\u2013196."},{"key":"e_1_3_3_18_2","first-page":"90","volume-title":"Proceedings of the Symposium on Logic in Computer Science (LICS)","author":"Bodirsky Manuel","year":"2010","unstructured":"Manuel Bodirsky, Martin Hils, and Barnaby Martin. 2010. On the scope of the universal-algebraic approach to constraint satisfaction. In Proceedings of the Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 90\u201399."},{"key":"e_1_3_3_19_2","first-page":"1","volume-title":"48th International Colloquium on Automata, Languages, and Programming, (ICALP \u201921)","volume":"120","author":"Bodirsky Manuel","year":"2021","unstructured":"Manuel Bodirsky, Simon Kn\u00e4uer, and Sebastian Rudolph. 2021. Datalog-expressibility for monadic and guarded second-order logic. In 48th International Colloquium on Automata, Languages, and Programming, (ICALP \u201921), Article 120, 1\u201317. DOI: 10.4230\/LIPIcs.ICALP.2021.120"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exi083"},{"issue":"1","key":"e_1_3_3_21_2","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1017\/jsl.2019.23","article-title":"Projective clone homomorphisms","volume":"86","author":"Bodirsky Manuel","year":"2021","unstructured":"Manuel Bodirsky, Michael Pinsker, and Andr\u00e1s Pongr\u00e1cz. 2021. Projective clone homomorphisms. Journal of Symbolic Logic 86, 1 (2021), 148\u2013161.","journal-title":"Journal of Symbolic Logic"},{"key":"e_1_3_3_22_2","first-page":"2826","volume-title":"Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI \u201915)","author":"Bourhis Pierre","year":"2015","unstructured":"Pierre Bourhis, Markus Kr\u00f6tzsch, and Sebastian Rudolph. 2015. Reasonable highly expressive query languages\u2014IJCAI-15 distinguished paper (honorary mention). In Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI \u201915). AAAI Press, 2826\u20132832."},{"key":"e_1_3_3_23_2","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1109\/FOCS.2017.37","volume-title":"58th IEEE Annual Symposium on Foundations of Computer Science (FOCS \u201917)","author":"Bulatov Andrei A.","year":"2017","unstructured":"Andrei A. Bulatov. 2017. A dichotomy theorem for nonuniform CSPs. In 58th IEEE Annual Symposium on Foundations of Computer Science (FOCS \u201917), 319\u2013330."},{"key":"e_1_3_3_24_2","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1007\/BF01446598","article-title":"\u00dcber unendliche, lineare punktmannigfaltigkeiten","volume":"23","author":"Cantor Georg","year":"1884","unstructured":"Georg Cantor. 1884. \u00dcber unendliche, lineare punktmannigfaltigkeiten. Mathematische Annalen 23 (1884), 453\u2013488.","journal-title":"Mathematische Annalen"},{"key":"e_1_3_3_25_2","doi-asserted-by":"crossref","first-page":"3188","DOI":"10.1016\/j.tcs.2010.05.016","article-title":"CSP duality and trees of bounded pathwidth","volume":"411","author":"Carvalho Catarina","year":"2010","unstructured":"Catarina Carvalho, V\u00edctor Dalmau, and Andrei Krokhin. 2010. CSP duality and trees of bounded pathwidth. Theoretical Computer Science 411 (2010), 3188\u20133208.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"e_1_3_3_26_2","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1093\/logcom\/exr039","article-title":"Arc consistency and friends","volume":"23","author":"Chen H.","year":"2013","unstructured":"H. Chen, V. Dalmau, and B. Grussien. 2013. Arc consistency and friends. Journal of Logic and Computation 23, 1 (2013), 87\u2013108.","journal-title":"Journal of Logic and Computation"},{"key":"e_1_3_3_27_2","doi-asserted-by":"crossref","first-page":"454","DOI":"10.1006\/aama.1998.0641","article-title":"Universal graphs with forbidden subgraphs and algebraic closure","volume":"22","author":"Cherlin Gregory","year":"1999","unstructured":"Gregory Cherlin, Saharon Shelah, and Niangdong Shi. 1999. Universal graphs with forbidden subgraphs and algebraic closure. Advances in Applied Mathematics 22 (1999), 454\u2013491.","journal-title":"Advances in Applied Mathematics"},{"key":"e_1_3_3_28_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511977619","volume-title":"Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach","author":"Courcelle Bruno","year":"2012","unstructured":"Bruno Courcelle and Joost Engelfriet. 2012. Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Cambridge University Press, New York, NY."},{"key":"e_1_3_3_29_2","first-page":"310","volume-title":"Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP)","author":"Dalmau Victor","year":"2002","unstructured":"Victor Dalmau, Phokion G. Kolaitis, and Moshe Y. Vardi. 2002. Constraint satisfaction, bounded treewidth, and finite-variable logics. In Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP), 310\u2013326,."},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/502807.502810"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0515-9"},{"key":"e_1_3_3_32_2","doi-asserted-by":"crossref","unstructured":"Michael Elberfeld Martin Grohe and Till Tantau. 2012. Where first-order and monadic second-order logic coincide. arXiv:1204.6291. Retrieved from https:\/\/arxiv.org\/abs\/1204.6291","DOI":"10.1109\/LICS.2012.37"},{"key":"e_1_3_3_33_2","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1137\/S0097539794266766","article-title":"The computational structure of monotone monadic SNP and constraint satisfaction: A study through datalog and group theory","volume":"28","author":"Feder Tom\u00e1s","year":"1999","unstructured":"Tom\u00e1s Feder and Moshe Y. Vardi. 1999. The computational structure of monotone monadic SNP and constraint satisfaction: A study through datalog and group theory. SIAM Journal on Computing 28 (1999), 57\u2013104.","journal-title":"SIAM Journal on Computing"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-15(2:15)2019"},{"key":"e_1_3_3_35_2","unstructured":"Thomas Feller Tim S. Lyon Piotr Ostropolski-Nalewaja and Sebastian Rudolph. 2023. Decidability of querying first-order theories via countermodels of finite width. arXiv:2304.06348. Retrieved from https:\/\/arxiv.org\/abs\/2304.06348"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICDT.2023.18"},{"issue":"3","key":"e_1_3_3_37_2","doi-asserted-by":"crossref","first-page":"418","DOI":"10.1145\/507382.507388","article-title":"Back and forth between guarded and modal logics","volume":"3","author":"Gr\u00e4del Erich","year":"2002","unstructured":"Erich Gr\u00e4del, Colin Hirsch, and Martin Otto. 2002. Back and forth between guarded and modal logics. ACM Transactions on Computational Logic 3, 3 (2002), 418\u2013463.","journal-title":"ACM Transactions on Computational Logic"},{"key":"e_1_3_3_38_2","volume-title":"A Shorter Model Theory","author":"Hodges Wilfrid","year":"1997","unstructured":"Wilfrid Hodges. 1997. A Shorter Model Theory. Cambridge University Press, Cambridge."},{"issue":"1","key":"e_1_3_3_39_2","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1006\/jcss.1995.1055","article-title":"On the expressive power of datalog: Tools and a case study","volume":"51","author":"Kolaitis Phokion G.","year":"1995","unstructured":"Phokion G. Kolaitis and Moshe Y. Vardi. 1995. On the expressive power of datalog: Tools and a case study. Journal of Computer and System Sciences 51, 1 (1995), 110\u2013134.","journal-title":"Journal of Computer and System Sciences"},{"key":"e_1_3_3_40_2","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/2933575.2934510","volume-title":"Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201916)","author":"Kozik Marcin","year":"2016","unstructured":"Marcin Kozik. 2016. Weak consistency notions for all the CSPs of bounded width. In Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201916), 633\u2013641."},{"key":"e_1_3_3_41_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07003-1","volume-title":"Elements of Finite Model Theory","author":"Libkin Leonid","year":"2004","unstructured":"Leonid Libkin. 2004. Elements of Finite Model Theory. Springer."},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2021.138"},{"issue":"3","key":"e_1_3_3_43_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1379759.1379763","article-title":"Homomorphism preservation theorems","volume":"55","author":"Rossman Benjamin","year":"2008","unstructured":"Benjamin Rossman. 2008. Homomorphism preservation theorems. Journal of the ACM 55, 3 (2008) 1\u201353.","journal-title":"Journal of the ACM"},{"key":"e_1_3_3_44_2","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/2463664.2465227","volume-title":"Proceedings of the 32nd Symposium on Principles of Database Systems (PODS \u201913)","author":"Rudolph Sebastian","year":"2013","unstructured":"Sebastian Rudolph and Markus Kr\u00f6tzsch. 2013. Flag and check: Data access with monadically defined queries. In Proceedings of the 32nd Symposium on Principles of Database Systems (PODS \u201913). ACM, 151\u2013162. DOI: 10.1145\/2463664.2465227"},{"key":"e_1_3_3_45_2","first-page":"1","volume-title":"27th International Conference on Database Theory (ICDT \u201924)","author":"ten Cate Balder","year":"2024","unstructured":"Balder ten Cate, V\u00edctor Dalmau, and Jakub Oprsal. 2024. Right-adjoints for datalog programs. In 27th International Conference on Database Theory (ICDT \u201924). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Article 10, 1\u201320."},{"key":"e_1_3_3_46_2","unstructured":"Dmitriy Zhuk and Barnaby Martin. 2021. The complete classification for quantified equality constraints. arXiv:2104.00406. Retrieved from https:\/\/arxiv.org\/abs\/2104.00406"},{"key":"e_1_3_3_47_2","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1109\/FOCS.2017.38","volume-title":"58th IEEE Annual Symposium on Foundations of Computer Science (FOCS \u201917)","author":"Zhuk Dmitriy N.","year":"2017","unstructured":"Dmitriy N. Zhuk. 2017. A proof of CSP dichotomy conjecture. In 58th IEEE Annual Symposium on Foundations of Computer Science (FOCS \u201917), 331\u2013342. Retrieved from https:\/\/arxiv.org\/abs\/1704.01914"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779418","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T12:29:45Z","timestamp":1770899385000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779418"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2,12]]},"references-count":46,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,4,30]]}},"alternative-id":["10.1145\/3779418"],"URL":"https:\/\/doi.org\/10.1145\/3779418","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2,12]]},"assertion":[{"value":"2024-06-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-02-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}