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 $ın$ , there exists a canonical Datalog program $\Pi$ of width (��,k), that is, a Datalog program of width (��,k) which is sound for C (i.e., $\Pi$ only derives the goal predicate on a finite structure �� if �� $ın$ C) and with the property that $\Pi$ 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 $ømega$-categorical structures.
Links and resources
Tags
