Datalog-Expressibility for Monadic and Guarded Second-Order Logic

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 \({\mathcal{C}}\) of finite structures that can be expressed in MSO and is closed under homomorphisms, and for all \(\ell,k\in{\mathbb{N}}\) , there exists a canonical Datalog program \(\Pi\) of width \((\ell,k)\) 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 \({\mathcal{C}}\) in GSO whose complement is closed under homomorphisms is a finite union of constraint satisfaction problems (CSPs) of \(\omega\) -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 (GQ \({}^{+}\) ) . 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 GQ \({}^{+}\) .

Keywords

Affiliated Institutions

• Technische Universität Dresden DE

Related Publications