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 C of finite structures that can be expressed in MSO and is closed under homomorphisms, and for all integers l,k, there exists a canonical Datalog program Pi of width (l,k) 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 C 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 query in the intersection of MSO and Datalog that is not expressible in nested guarded queries.
Cite
@article{arxiv.2010.05677,
title = {Datalog-Expressibility for Monadic and Guarded Second-Order Logic},
author = {Manuel Bodirsky and Simon Knäuer and Sebastian Rudolph},
journal= {arXiv preprint arXiv:2010.05677},
year = {2025}
}
Comments
Some of the results of this article until Section 5 have been announced in a conference paper with the same title in the proceedings of ICALP'21; the results in Section 6 about nested monadic and nested guarded queries were not yet present in the conference version. The article has been accepted for publication in ACM Transactions of Computational Logic