%0 Conference Paper %1 Bodirsky2021-bz %A Bodirsky, Manuel %A Knäuer, Simon %A Rudolph, Sebastian %D 2021 %I Schloss Dagstuhl - Leibniz-Zentrum für Informatik %K %T Datalog-expressibility for monadic and Guarded Second-order Logic %X 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.

@inproceedings{Bodirsky2021-bz, 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 $\in$ , 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 �� $\in$ 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 $\omega$-categorical structures.}, added-at = {2024-09-10T11:56:37.000+0200}, author = {Bodirsky, Manuel and Kn{\"a}uer, Simon and Rudolph, Sebastian}, biburl = {https://puma.scadsai.uni-leipzig.de/bibtex/2cde5926de2f4a825d4b0159a8b12a66c/scadsfct}, interhash = {620e22f29991045610c351d50fda6343}, intrahash = {cde5926de2f4a825d4b0159a8b12a66c}, keywords = {}, month = jul, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik}, timestamp = {2024-09-10T15:15:57.000+0200}, title = {Datalog-expressibility for monadic and Guarded Second-order Logic}, year = 2021 }