Preferential low complexity description logics: Complexity results and proof methods

In this paper we describe an approach for reasoning about typicality and defeasible properties in low complexity preferential Description Logics. We describe the non-monotonic extension of the low complexity DLs EL⊥ And DL-Litecore based on a typicality operator T, which enjoys a preferential semantics. We summarize complexity results for such extensions, called EL⊥Tmin and DL-LitecTmin. Entailment in DL-LitecTmin is in IIp2 , whereas entailment in EL⊥Tmin is EXPTIME-hard.However, for the Left Local fragment of EL⊥Tmin the complexity of entailment drops to Ip2 . We present tableau calculi for Left Local EL⊥Tmin and for 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, and provide decision procedures for verifying entailment in the two logics, whose complexities match the above mentioned complexity results.