Prime implicate normal form for ALC concepts: Long version

In this paper, we present a normal form for concept expres-sions in the description logic ALC which is based on a re-cently introduced notion of prime implicate for the modal logic K. We show that concepts in prime implicate nor-mal form enjoy a number of desirable properties which make prime implicate normal form interesting from the viewpoint of knowledge compilation. In particular, we prove that sub-sumption between ALC concepts in prime implicate normal form can be carried out in polynomial time using a simple structural subsumption algorithm reminiscent of those used for less expressive description logics. Of course, in order to take advantage of these properties, we need a way to trans-form concepts into equivalent concepts in prime implicate normal form. We provide a sound and complete algorithm for putting concepts into prime implicate normal form, and we investigate the spatial complexity of this transformation, showing there to be an at most doubly-exponential blowup in concept length. At the end of the paper, we compare prime implicate normal form to two other normal forms for ALC, discussing the relative merits of the different approaches