Pointwise circumscription in description logics

Circumscription is one of the major approaches to bring non-monotonic (common-sense) reasoning features to first-order logic and related formalisms, and it has already received attention in Description Logics (DLs), with the focus on understanding the computational complexity of reasoning. Those studies revealed that circumscription causes a dramatic increase in computational complexity in a broad range of DLs. In this paper, we consider a new notion of circumscription in DLs, aiming to preserve the key ideas and advantages of classical circumscription while mitigating its impact on the computational complexity of reasoning. 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. This approach provides a sound approximation of classical circumscription and is closely related to the notion of pointwise circumscription proposed by Lifschitz for first-order logic. Our main achievement is to show that, under certain syntactic restrictions, standard reasoning problems like subsumption testing or concept satisfiability for AℒCℐO KBs with pointwise circumscription are (co)NExpTime-complete