A tableau calculus for a nonmonotonic extension of EL^\bot

We introduce a tableau calculus for a nonmonotonic extension of low complexity Description Logic EL\bot that can be used to reason about typicality and defeasible properties. The calculus deals with Left Local knowledge bases in the logic EL\botTmin recently introduced. 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 EL\botTmin knowledge bases, whose complexity matches the known results for the logic, namely that entailment is in \Pi^p_2 .