We introduce a tableau calculus for a nonmonotonic extension of low complexity Description Logic εL~⊥ that can be used to reason about typicality and defeasible properties. The calculus deals with Left Local knowledge bases in the logic εL~⊥T_(min) recently introduced in [8]. 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 Left Local εL~⊥T_(min) knowledge bases, whose complexity matches the known results for the logic, namely that entailment is in Π_2~p.
展开▼
