Adding Circumscription to Decidable Fragments of First-Order Logic: A Complexity Rollercoaster
This work addresses foundational issues in automated reasoning and knowledge representation, providing complexity results for circumscription in decidable logics, which is incremental but with notable complexity jumps.
The paper tackles the problem of extending decidable fragments of first-order logic with circumscription, showing that decidability is preserved when minimizing unary predicates, but complexity increases significantly, such as from coNexp to coNExp^NP-complete for FO^2 and from 2Exp to Tower-complete for GF.
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.