A connection method for a defeasible extension of ALC

In this paper, we propose a connection method `a la Bibel for an exception-tolerant extension of ALC. As for the language, we assume ALC extended with a typicality operator on concepts, which is a variant of defeasible DLs studied in the literature over the past decade and in which most of these can be embedded. We revisit the definition of matrix representation of a knowledge base and establish the conditions for a given axiom to be provable from it. In particular, we show how term substitution is dealt with and define a suitable condition of blocking in the presence of typicality operators. We show that the calculus terminates and that it is sound and complete w.r.t. a DL version of the preferential semantics widely adopted in non-monotonic reasoning.