A Tableau Calculus for a Nonmonotonic Extension of the Description Logic $\mbox{\em DL-Lite}_{\mathit{core}}$

In this paper we introduce a tableau calculus for a nonmonotonic extension of the low complexity Description Logic DL-Litecore of the DL-Litecore family. The extension, called DL-LitecTmin, can be used to reason about typicality and defeasible properties. The calculus performs a two-phase computation to check whether a query is minimally entailed from the initial knowledge base. It is sound, complete and terminating. Furthermore, it is a decision procedure for DL-LitecTmin knowledge bases, whose complexity matches the known results for the logic, namely that entailment is in Π2p.