Subsumption algorithms for concept description languages

Abstract

We investigate subsumption algorithms for logic-based knowledge representation languages of the kl-one family. We define an attributive concept description language that contains the logical connectives conjunction, disjunction, and negation, as well as role quantification, number restrictions and role intersection. We describe a rule based calculus to decide subsumption in this language, that closely resembles the tableaux calculus of first order predicate logic. Furthermore, we give polynomial space algorithms for certain sublanguages. 1 Introduction Concept description languages of the kl-one family are a means of expressing taxonomical knowledge by describing hierarchies of concepts [1, 2, 4, 6, 11]. Concepts are described as specializations of other concepts and by the values of attributes (so-called roles). In contrast to earlier knowledge representation formalisms like frames and semantic networks, kl-one languages have the advantage of a Tarski style declarative semantics th...