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

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 coNexp to coNExp^NP-complete, for GF it (remarkably!) increases from 2Exp to 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, 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 0 there is an ontology and query that are k-Exp-hard in data complexity.

Tasks

Reproductions