Datalog-Expressibility for Monadic and Guarded Second-Order Logic

Manuel BodirskyManuel Bodirsky, Simon KnäuerSimon Knäuer, Sebastian RudolphSebastian Rudolph

Manuel Bodirsky, Simon Knäuer, Sebastian Rudolph
Datalog-Expressibility for Monadic and Guarded Second-Order Logic
In Nikhil Bansal, James Worrell, eds., Proceedings of the 48th International Colloquium on Automata, Languages, and Programming (ICALP), LIPIcs, 120:1-120:17, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik

Details
Bibtex

KurzfassungAbstract
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 𝒞 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 𝒞 (i.e., Π only derives the goal predicate on a finite structure 𝔄 if 𝔄 ∈ 𝒞) and with the property that Π derives the goal predicate whenever some Datalog program of width (ℓ,k) which is sound for 𝒞 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 𝒞 in GSO whose complement is closed under homomorphisms is a finite union of constraint satisfaction problems (CSPs) of ω-categorical structures.
Weitere Informationen unter:Further Information: Link
Projekt:Project: DeciGUT
Forschungsgruppe:Research Group: Algebra und Diskrete StrukturenAlgebra and Discrete Structures, Computational LogicComputational Logic

@inproceedings{BKR2021,
  author    = {Manuel Bodirsky and Simon Kn{\"{a}}uer and Sebastian Rudolph},
  title     = {Datalog-Expressibility for Monadic and Guarded Second-Order Logic},
  editor    = {Nikhil Bansal and James Worrell},
  booktitle = {Proceedings of the 48th International Colloquium on Automata,
               Languages, and Programming (ICALP)},
  series    = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2021},
  pages     = {120:1-120:17},
  doi       = {10.4230/LIPIcs.ICALP.2021.120}
}