Document Open Access Logo

Datalog-Expressibility for Monadic and Guarded Second-Order Logic

Authors Manuel Bodirsky , Simon Knäuer, Sebastian Rudolph

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2021.120.pdf
  • Filesize: 0.73 MB
  • 17 pages

Document Identifiers

Author Details

Manuel Bodirsky
  • Institut für Algebra, TU Dresden, Germany
Simon Knäuer
  • Institut für Algebra, TU Dresden, Germany
Sebastian Rudolph
  • Computational Logic Group, TU Dresden, Germany

Funding

  • Bodirsky, Manuel: The author has received funding from the European Research Council (Grant Agreement no. 681988, CSP-Infinity).
  • Knäuer, Simon: The author is supported by DFG Graduiertenkolleg 1763 (QuantLA).
  • Rudolph, Sebastian: The author has received funding from the European Research Council (Grant Agreement no. 771779, DeciGUT).

Cite AsGet BibTex

Manuel Bodirsky, Simon Knäuer, and Sebastian Rudolph. Datalog-Expressibility for Monadic and Guarded Second-Order Logic. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 120:1-120:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ICALP.2021.120

Abstract

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 C of finite structures that can be expressed in MSO and is closed under homomorphisms, and for all 𝓁,k ∈ , there exists a canonical Datalog program Π of width (𝓁,k), that is, a Datalog program of width (𝓁,k) which is sound for C (i.e., Π only derives the goal predicate on a finite structure 𝔄 if 𝔄 ∈ C) and with the property that Π derives the goal predicate whenever some Datalog program of width (𝓁,k) which is sound for C derives the goal predicate. The same characterisations also hold for Guarded Second-order Logic (GSO), which properly extends MSO. To prove our results, we show that every class C in GSO whose complement is closed under homomorphisms is a finite union of constraint satisfaction problems (CSPs) of ω-categorical structures.

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
Keywords
  • Monadic Second-order Logic
  • Guarded Second-order Logic
  • Datalog
  • constraint satisfaction
  • homomorphism-closed
  • conjunctive query
  • primitive positive formula
  • pebble game
  • ω-categoricity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Hajnal Andréka, István Németi, and Johan van Benthem. Modal languages and bounded fragments of predicate logic. J. Philos. Log., 27(3):217-274, 1998. URL: https://doi.org/10.1023/A:1004275029985.
  2. Albert Atserias, Andrei A. Bulatov, and Anuj Dawar. Affine systems of equations and counting infinitary logic. Theoretical Computer Science, 410(18):1666-1683, 2009. Google Scholar
  3. Libor Barto and Marcin Kozik. Constraint satisfaction problems solvable by local consistency methods. Journal of the ACM, 61(1):3:1-3:19, 2014. Google Scholar
  4. Christoph Berkholz. Lower bounds for existential pebble games and k-consistency tests. Log. Methods Comput. Sci., 9(4), 2013. URL: https://doi.org/10.2168/LMCS-9(4:2)2013.
  5. Achim Blumensath. Monadic second-order logic. Lecture Notes, 2020. Google Scholar
  6. Manuel Bodirsky. Complexity of infinite-domain constraint satisfaction. To appear in the LNL Series, Cambridge University Press, 2021. Google Scholar
  7. Manuel Bodirsky and Víctor Dalmau. Datalog and constraint satisfaction with infinite templates. Journal on Computer and System Sciences, 79:79-100, 2013. A preliminary version appeared in the proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS'05). Google Scholar
  8. Manuel Bodirsky, Thomas Feller, Simon Knäuer, and Sebastian Rudolph. On logics and homomorphism closure. In Proceedings of the Symposium on Logic in Computer Science (LICS), 2021. Preprint URL: https://arxiv.org/abs/2104.11955.
  9. Manuel Bodirsky and Martin Grohe. Non-dichotomies in constraint satisfaction complexity. In Luca Aceto, Ivan Damgard, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP), Lecture Notes in Computer Science, pages 184-196. Springer Verlag, July 2008. Google Scholar
  10. Manuel Bodirsky, Martin Hils, and Barnaby Martin. On the scope of the universal-algebraic approach to constraint satisfaction. In Proceedings of the Symposium on Logic in Computer Science (LICS), pages 90-99. IEEE Computer Society, July 2010. Google Scholar
  11. Manuel Bodirsky, Wied Pakusa, and Jakub Rydval. Temporal constraint satisfaction problems in fixed-point logic. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 237-251. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394750.
  12. Manuel Bodirsky, Michael Pinsker, and András Pongrácz. Projective clone homomorphisms. Journal of Symbolic Logic, pages 1-13, 2019. doi:10.1017/jsl.2019.23. Google Scholar
  13. Pierre Bourhis, Markus Krötzsch, and Sebastian Rudolph. Reasonable highly expressive query languages - IJCAI-15 distinguished paper (honorary mention). In Qiang Yang and Michael J. Wooldridge, editors, Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 2826-2832. AAAI Press, 2015. Google Scholar
  14. Andrei A. Bulatov. A dichotomy theorem for nonuniform CSPs. In 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, pages 319-330, 2017. Google Scholar
  15. Georg Cantor. Über unendliche, lineare Punktmannigfaltigkeiten. Mathematische Annalen, 23:453-488, 1884. Google Scholar
  16. Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Cambridge University Press, 40 W. 20 St. New York, NY, United States, 2012. Google Scholar
  17. Victor Dalmau, Phokion G. Kolaitis, and Moshe Y. Vardi. Constraint satisfaction, bounded treewidth, and finite-variable logics. In Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP), pages 310-326, 2002. Google Scholar
  18. Michael Elberfeld, Martin Grohe, and Till Tantau. Where first-order and monadic second-order logic coincide. CoRR, abs/1204.6291, 2012. URL: http://arxiv.org/abs/1204.6291.
  19. Tomás Feder and Moshe Y. Vardi. The computational structure of monotone monadic SNP and constraint satisfaction: a study through Datalog and group theory. SIAM Journal on Computing, 28:57-104, 1999. Google Scholar
  20. Erich Grädel. Description logics and guarded fragments of first order logic. In Enrico Franconi, Giuseppe De Giacomo, Robert M. MacGregor, Werner Nutt, and Christopher A. Welty, editors, Proceedings of the 1998 International Workshop on Description Logics (DL'98), IRST, Povo - Trento, Italy, June 6-8, 1998, volume 11 of CEUR Workshop Proceedings. CEUR-WS.org, 1998. URL: http://ceur-ws.org/Vol-11/graedel.ps.
  21. Erich Grädel, Colin Hirsch, and Martin Otto. Back and forth between guarded and modal logics. ACM Trans. Comput. Log., 3(3):418-463, 2002. Google Scholar
  22. Wilfrid Hodges. A shorter model theory. Cambridge University Press, Cambridge, 1997. Google Scholar
  23. Phokion G. Kolaitis and Moshe Y. Vardi. On the expressive power of Datalog: Tools and a case study. Journal of Computer and System Sciences, 51(1):110-134, 1995. Google Scholar
  24. Leonid Libkin. Elements of Finite Model Theory. Springer, 2004. Google Scholar
  25. Sebastian Rudolph and Markus Krötzsch. Flag & check: Data access with monadically defined queries. In Proc. 32nd Symposium on Principles of Database Systems (PODS'13), pages 151-162. ACM, June 2013. URL: https://doi.org/10.1145/2463664.2465227.
  26. Dmitriy N. Zhuk. A proof of CSP dichotomy conjecture. In 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, pages 331-342, 2017. URL: http://arxiv.org/abs/1704.01914.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact