Preferential Tableaux for Contextual Defeasible ALC.

In recent work, we addressed an important limitation in previous extensions of description logics to represent defeasible knowledge, namely the restriction in the semantics of defeasible concept inclusion to a single preference order on objects of the domain. Syntactically, this limitation translates to a context-agnostic notion of defeasible subsumption, which is quite restrictive when it comes to modelling different nuances of defeasibility. Our point of departure in our recent proposal allows for different orderings on the interpretation of roles. This yields a notion of contextual defeasible subsumption, where the context is informed by a role. In the present paper, we extend this work to also provide a proof-theoretic counterpart and associated results. We define a (naive) tableau-based algorithm for checking preferential consistency of contextual defeasible knowledge bases, a central piece in the definition of other forms of contextual defeasible reasoning over ontologies, notably contextual rational closure.