Prime Implicate Normal Form for ALC Concepts

In this paper, we present a normal form for concept expressions in the description logicALC which is based on a recently introduced notion of prime implicate for the modal logicK. We show that con- cepts in prime implicate normal form enjoy a number of interesting properties. For one thing, they do not contain any unnecessary atomic concepts or roles. Not only does this make the concept more readable but it also helps us to identify the parts of a concept which are rele- vant to a given subject matter. Another feature of concepts in prime implicate normal form is that they can be easily approximated over a sublanguage or up to a xed depth. These operations may prove useful when a concept description is too large to be fully understood or when data needs to be exchanged between systems using dierent languages. Perhaps the most remarkable property of prime implicate normal form is that subsumption betweenALC concepts in this form can be carried out in quadratic time using a simple structural subsumption algorithm reminiscent of those used for less expressive description logics. This property makes prime implicate normal form interesting for the pur- poses of knowledge compilation. Of course, in order to take advantage of all of these nice properties, we need a way to transform concepts into equivalent concepts in prime implicate normal form. We provide a sound and complete algorithm for putting concepts into prime im- plicate normal form, and we investigate the spatial complexity of this transformation, showing there to be an at most doubly-exponential blowup in concept size. At the end of the paper, we compare prime implicate normal form to two other normal forms for ALC concepts that have been proposed in the literature, discussing the relative mer- its of the dierent approaches.