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

In this paper we propose nonmonotonic extensions of low complexity Description Logics εL⊥ and DL-Lite_core for reasoning about typicality and defeasible properties. The resulting logics are called εL⊥_min and DL-Lite_cT_min. We summarize complexity results for such extensions recently studied. Entail-ment in DL-Lite_cT_min is in II₂^p, whereas entailment in εL⊥_min is EXPTIME-hard. However, considering the known fragment of Left Local εL⊥T_min, we have that the complexity of entailment drops to II₂^p. Furthermore, we present tableau calculi for εL⊥T_min (focusing on Left Local knowledge bases) and DL-Lite_cT_min. 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 εL⊥T_min knowledge bases and DL-Lite_cT _min knowledge bases, whose complexities match the above mentioned results.