Datalog-Expressibility for Monadic and Guarded Second-Order Logic

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

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 Π of width (ℓ, k), that is, a Datalog program of width (ℓ, k) which is sound for C (i.e., Π only derives the goal predicate on a finite structure A if A ∈ C) and with the property that Π 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 ω-categorical structures.

Details

OriginalspracheEnglisch
Titel48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)
Redakteure/-innenNikhil Bansal, Emanuela Merelli, James Worrell
Herausgeber (Verlag)Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Seiten120:1-120:17
Seitenumfang17
ISBN (Print)978-3-95977-195-5
PublikationsstatusVeröffentlicht - 1 Juli 2021
Peer-Review-StatusJa

Externe IDs

Scopus 85106412752
ORCID /0000-0001-8228-3611/work/142241053

Schlagworte

ASJC Scopus Sachgebiete

Schlagwörter

  • Conjunctive query, Constraint satisfaction, Datalog, Guarded second-order logic, Homomorphism-closed, Monadic second-order logic, Pebble game, Primitive positive formula, ω-categoricity