Nonmonotonic extensions of low-complexity DLs: complexity results and proof methods

In this paper we propose nonmonotonic extensions of low complexity Description Logics EL\bot and DL-Litecore for reasoning about typicality and defeasible properties. The resulting logics are called EL\botTmin and DL-LitecTmin. We summarize complexity results for such extensions recently studied. Entailment in DL-LitecTmin is in \Pi^2_2, whereas entailment in EL\botTmin is EXPTIMEhard. However, considering the known fragment of Left Local EL\botTmin, we have that the complexity of entailment drops to \Pi^p_2. Furthermore, we present tableau calculi for EL\botTmin (focusing on Left Local knowledge bases) and DL-LitecTmin. The calculi perform a two-phase computation in order to check whether a query is minimally entailed from the initial knowledge base. The calculi are sound, complete and terminating. Furthermore, they represent decision procedures for Left Local EL\botTmin knowledge bases and DL-LitecTmin knowledge bases, whose complexities match the above mentioned results.