Description Logics with Pointwise Circumscription

Circumscription is one of the most expressive means to bring non-monotonic (common-sense) reasoning features to first-order logic and related formalisms. But unfortunately, the high expressiveness comes with high computational costs. In Description Logics (DLs), which in most cases are decidable fragments of first-order logic, circumscription often leads to undecidability or very high computational complexity of the basic reasoning problems. In this paper, we consider a new notion of circumscription for DLs, aiming to preserve the key ideas and advantages of classic circumscription while mitigating its impact on the computational complexity of reasoning. Specifically, we introduce pointwise circumscription for DLs, which is not only intuitive in terms of knowledge representation, but also provides a sound approximation of classic circumscription. Our main idea is to replace the second-order quantification step with a series of (pointwise) local checks on all domain elements and their immediate neighborhood. After defining this notion, we study its computational complexity for standard reasoning tasks (like checking concept satisfiability, concept subsumption, instance checking), under a couple of syntactic restrictions. Our main positive decidability and complexity results are for TBoxes of modal depth 1 (i.e. without nesting of existential or universal quantifiers) in the DLs ALCIO and ALCI, with (co)NEXPTIME-completeness and EXPTIME-completeness, respectively. This class of TBoxes is large and relevant in practice (e.g., the popular DLs of the DL-Lite family also disallow nesting of quantifiers). These upper bounds are obtained by a sophisticated reduction to integer programming. Finally, as an additional justification for the considered syntactic restriction, we provide a strong undecidability result for pointwise circumscription with general TBoxes (with modal depth greater than 1).