A computationally tractable terminological logic

Terminological Logics are knowledge representation formalisms of enormous applicative interest, as they are specifically oriented to the vast class of application domains that are describable by means of taxonomic organizations of complex objects. A number of results relative to the computationa1 complexity of terminologica1 logics have recently appeared in the literature. Unfortunately, most of these results are "negative" in nature, as they show that, in the logics they refer to, deciding subsumption (i.e. the metalinguistic relation which corresponds to validity in standard logics) is computationally intractable. In this paper, after briefly introducing the fundamental concepts underlying terminologica1 logics, we show that computing subsumption is O(n log n) in the ALN logic, an extension of Brachman and Levesque's FL?- logic. ANL is obtained by endowing :FL?- with the two operators atleast and atmost, which allow the specification of number restrictions, and the operator a-not, which introduces a limited form of negation. The result we present is of theoretica1 significance, in that ALN is one of the few terminologica1 logics that have been shown tractable. ALN is a1so a pragmatically significant extension of FL?-, as it results from the addition of operators of considerable applicative interest.