Adding Circumscription to Decidable Fragments of First-Order Logic: A Complexity Rollercoaster

TL;DR

This paper investigates the effects of adding circumscription to decidable first-order logic fragments, focusing on $FO^2$, $C^2$, and GF. It shows that restricting circumscription to unary minimized/fixed predicates preserves decidability and yields fragment-specific complexity increases: circumscribed consequence for $FO^2$ is $ ext{coNExp}^{ ext{NP}}$-complete, while for GF the complexity soars to Tower-complete; $C^2$ remains decidable but its exact complexity is open. For circumscribed querying on GF ontologies, the authors obtain Tower-complete combined complexity and Elementary data complexity for UCQs, with lower bounds from guarded existential rules. The work further provides methodology to obtain finite-model properties for circumscribed GF via Rosati covers and mosaic techniques, and uses reductions to Presburger arithmetic to establish decidability for $C^2$ circumscription. Overall, the results reveal a striking heterogeneity in complexity across fragments and raise open questions about optimal bounds and finite controllability in circumscribed GF and $C^2$.

Abstract

We study extensions of expressive decidable fragments of first-order logic with circumscription, in particular the two-variable fragment FO$^2$, its extension C$^2$ with counting quantifiers, and the guarded fragment GF. We prove that if only unary predicates are minimized (or fixed) during circumscription, then decidability of logical consequence is preserved. For FO$^2$ the complexity increases from $\textrm{coNexp}$ to $\textrm{coNExp}^\textrm{NP}$-complete, for GF it (remarkably!) increases from $\textrm{2Exp}$ to $\textrm{Tower}$-complete, and for C$^2$ the complexity remains open. We also consider querying circumscribed knowledge bases whose ontology is a GF sentence, showing that the problem is decidable for unions of conjunctive queries, $\textrm{Tower}$-complete in combined complexity, and elementary in data complexity. Already for atomic queries and ontologies that are sets of guarded existential rules, however, for every $k \geq 0$ there is an ontology and query that are $k$-$\textrm{Exp}$-hard in data complexity.

Figures (4)

• Figure 1: Additional rules used in the proof of Theorem \ref{['theorem:tower-hardness']} for every $k \in \{ 2, \dots, \kappa\}$.
• Figure 2: Inductive case on both $m$ and $n$ in the proof of Lemma \ref{['lem:formerclaim']}. If $R(x_2, \delta, x_1, x_1, x_4) \in t$, we need to prove $R(x_2, \delta, x_3, x_3, x_1) \in t'$.
• Figure 3: Additional rules used in the proof of Theorem \ref{['theorem:exp-hardness']}, for all $i \in \{ 1, 2\}$.
• Figure 4: Additional rules used in the proof of Theorem \ref{['theorem:tower-hardness']} for every $k \in \{ 2, \dots, \kappa\}$.

Theorems & Definitions (54)

• Example 1
• Proposition 1
• Proposition 2
• proof
• Theorem 1
• proof
• Theorem 2
• proof
• Proposition 3
• Lemma 1