Prime Implicate Normal Form for ALC Concepts

Meghyn Bienvenu

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 concepts, discussing the relative merits of the different approaches.

Subjects: 11.1 Description Logics; 3. Automated Reasoning

Submitted: Apr 15, 2008


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.