A tableau calculus for a nonmonotonic extension of the Description Logic DL-Litecore

In this paper we introduce a tableau calculus for a nonmonotonic extension of the low complexity Description Logic DL-Litecore of the DL-Lite 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 \Pi^p_2.