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
ACM Transactions on Computational Logic, to appear

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 ℓ,𝑘, there exists a canonical Datalog program Π of width (ℓ,𝑘) in the sense of Feder and Verdi. 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. The intersection of MSO and Datalog is known to contain the class of nested monadically defined queries (Nemodeq); likewise, we show that the intersection of GSO and Datalog contains all problems that can be expressed by the more expressive language of nested guarded queries. Yet, by exploiting our results, we can show that neither of the two query languages can serve as a characterization, as we exhibit a CSP whose complement corresponds to a query in the intersection of MSO and Datalog that is not expressible in nested guarded queries.
Weitere Informationen unter:Further Information: Link
Projekt:Project: DeciGUT
Forschungsgruppe:Research Group: Algebra und Diskrete StrukturenAlgebra and Discrete Structures, Computational LogicComputational Logic

@article{BKR2025,
  author    = {Manuel Bodirsky and Simon Kn{\"{a}}uer and Sebastian Rudolph},
  title     = {Datalog-Expressibility for Monadic and Guarded Second-Order Logic},
  journal   = {ACM Transactions on Computational Logic},
  publisher = {ACM},
  year      = {2025},
  doi       = {10.1145/3779418}
}