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

TL;DR

This paper explores how adding circumscription to certain decidable fragments of first-order logic affects their complexity and decidability, revealing significant complexity increases in some cases.

Contribution

It demonstrates that circumscription preserves decidability under unary predicate minimization and characterizes the resulting complexity changes for various logic fragments.

Findings

Decidability is preserved with unary predicate circumscription.

Complexity increases from coNexp to coNExp^NP for FO^2.

Complexity jumps to Tower-complete for GF fragment.

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.