Prime Implicate Normal Form for ALC Concepts

In this paper, we present a normal form for concept expressions in the description logic ALC which is based on a recently introduced notion of prime implicate for the modal logic K. We show that concepts in prime implicate normal 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 subsumption 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 transform 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.

Authors

• Meghyn Bienvenu

Keywords

No keywords are indexed for this paper.