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.
%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
}
