Datalog-Expressibility for Monadic and Guarded Second-Order Logic

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

Download

Manuel Bodirsky, Simon Knäuer, Sebastian Rudolph
Datalog-Expressibility for Monadic and Guarded Second-Order Logic
Technical Report, arXiv.org, volume 2010.05677, October 2020

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 integers l,k, there exists a canonical Datalog program Π of width (l,k), that is, a Datalog program of width (l,k) which is sound for 𝒞 (i.e., Π only derives the goal predicate on a finite structure 𝔄 if 𝔄 is in 𝒞) and with the property that Π derives the goal predicate whenever some Datalog program of width (l,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 countably categorical structures.
Weitere Informationen unter:Further Information: Link
Projekt:Project: DeciGUT, QuantLA
Forschungsgruppe:Research Group: Algebra und Diskrete StrukturenAlgebra and Discrete Structures, Computational LogicComputational Logic

@techreport{BKR2020,
  author      = {Manuel Bodirsky and Simon Kn{\"{a}}uer and Sebastian Rudolph},
  title       = {Datalog-Expressibility for Monadic and Guarded Second-Order
                 Logic},
  institution = {arXiv.org},
  year        = {2020},
  month       = {October}
}