
| Question              | Answer type      | Response               |                   |
|-----------------------|------------------|------------------------|-------------------|
| ask-subsumes?(C, D)   | Boolean          | true iff CKB |= C =⇒ D |                   |
| ask-ancestors(C)      | SET(ConceptName) | {CN ∈C                 | | CKB |= C =⇒ CN} |
| ask-is-incoherent?(C) | Boolean          | true iff CKB |= C      | =⇒ nothing        |

A number of other operations on concepts have been found to be **useful, including**
(i) computing the least common subsumer of two concepts (Cohen, Borgida, & Hirsh, 1992) (useful for machine learning), (ii) matching concepts against patterns (Borgida &
McGuinness, 1996) (useful in large KBs for viewing only relevant aspects of concepts), (iii)
finding what additional **information has been deduced about a concept or especially an** individual given the information in the KB (see Section 4.2).

To facilitate answering the above questions, and others like them, the DL-KBMS almost always performs concept classification**: named concepts ("classes") are organized into the**
so-called IsA hierarchy, finding for each class the most specific other classes that subsume it. The classification algorithm relies on the =⇒ **relationships, treating it as a subroutine,**
and as such is largely DL-independent. Interesting previous work in this area has been reported by Baader et al (Baader et al., 1994).

The KBMS is also charged with a number of clerical tasks, including keeping a symbol table of the declarations, maintaining and accessing efficiently the precomputed IsA hierarchy, signaling definitions/declarations that are redundant (i.e., a concept which is equivalent to a previously defined one) or are incoherent.

DL-KBMS perform inferences on individuals, as well as concepts. The operations involved will be described in Section 5.

## 2.4 Reasoning Strategies

There are two general approaches to answering the fundamental subsumption question underlying the DL-KBMS operations.

One approach is based on theorem proving techniques specially adapted for descriptions, particularly variants of tableau techniques that determine the subsumption A =⇒ **B by**
checking for the unsatisfiability of A∧¬B; systems such as kris (Baader et al., 1994),**crack** (Bresciani, Franconi, & Tessaris, 1995), FaCT (Horrocks, 1998) and DLP **(Patel-Schneider,**
1998) follow this approach. Such systems have the advantage **of being provably complete.** Although the worst-case complexity bounds of the subsumption problems are sometimes quite high (EXPTIME complete), recent empirical evidence shows that their performance for computing subsumption on large realistic KBs is quite effective (Horrocks & PatelSchneider, 1998).

All the implemented DL KBMS systems that have had wide distribution and use, such as back (von Luck et al., 1987), classic (Borgida et al., 1989), and loom **(MacGregor, 1986), follow a so-called "normalize-compare" paradigm, where most of the reasoning**
work is performed in an initial "normalization" phase, whose goal is to find a normal form for concepts which explicates implicit facts, eliminates redundancies and detects incoherencies. Once this is done, when, for example, it comes to comparing two concepts for subsumption, it is often (but not always) a matter of comparing only "structurally similar" elements - ones built with the same **constructor. For example, since the descriptions**