ALC+T: Reasoning About Typicality in Description Logics

We extend the Description Logic ALC with a “typicality” operator T that allows us to reason about the prototypical properties and inheritance with exceptions. The resulting logic is called ALC + T. The typicality operator is intended to select the “most normal” or “most typical” instances of a concept. In our framework, knowledge bases may then contain, in addition to ordinary ABoxes and TBoxes, subsumption relations of the form “T(C) is subsumed by P”, expressing that typical C-members have the property P. The semantics of a typicality operator is defined by a set of postulates that are strongly related to Kraus-Lehmann-Magidor axioms of preferential logic P. We first show that T enjoys a simple semantics provided by ordinary structures equipped by a preference relation. This allows us to obtain a modal interpretation of the typicality operator. Using such a modal interpretation, we present a tableau calculus for deciding satisfiability of ALC + T knowledge bases. Our calculus gives a nondeterministic-exponential time decision procedure for satisfiability of ALC + T. We then extend ALC + T knowledge bases by a nonmonotonic completion that allows inferring defeasible properties of specific concept instances. This paper has been also presented at the 14th Conference on Logic for Programming, Artificial Intelligence, and Reasoning “LPAR 2007”