A computationally tractable terminological logic.

In Proceedings of SCAI-91, 3rd Scandinavian Conference on Artificial Intelligence, pages 307--315, Roskilde, Denmark, 1991.

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 computational complexity of terminological 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 terminological logics, we show that computing subsumption is O(n log n) in the ALN logic, an extension of Brachman and Levesque's FL- logic. ALN 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 theoretical significance, in that ALN is one of the few terminological logics that have been shown tractable. ALN is also a pragmatically significant extension of FL-, as it results from the addition of operators of considerable applicative interest.