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

We study extensions of expressive decidable fragments of first-order logic with circumscription, in particular the two-variable fragment FO², its extension C² 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² the complexity increases from coNexp to coNExpNP-complete, for GF it (remarkably!) increases from 2Exp to Tower-complete, and for C² 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.