Definitorially Complete Description Logics.

The Terminology Box (TBox) of a Description Logic (DL) knowledge base is used to define new concepts in terms of primitive concepts and relations. The topic of this paper is the effect of the available operations in a DL on the length and the syntactic shape of definitions in a Terminology Box. Defining new concepts can be done in two ways: (1) in an explicit syntactical manner as in NewConcept ≐ C, with C an expression in which NewConcept does not occur. Acyclic TBoxes only contain such axioms. (2) implicitly, by writing a set of general inclusion axioms ⊤ with the property that in any model of ⊤, the interpretation of NewConcept is uniquely determined by the interpretation of the primitive concepts and relations. The explicit manner is preferred because its syntactic simplicity makes it immediately clear that NewConcept is nothing but a defined concept, and leads to algorithms with a lower worst case complexity. The focus of this paper is on the following property of DL's: every new concept defined in the implicit way can also be defined in the explicit manner. DL's with this property are called Definitorially Complete. It is known that ALC is definitorially complete. We provide a concrete algorithm for computing explicit definitions on the basis of implicit definitions. It involves at most a triply exponential blowup, and is based on a method for obtaining exponential size uniform interpolants. We also investigate definitorial completeness for a number of extensions of ALC . We show that definitorial completeness is preserved when ALC is extended with qualified number restrictions ( ALCQ ), but is lost when nominals are added ( ALCO ). On the other hand, definitorial completeness is regained when ALCO is further extended with the @-operator. We also show that all extensions of ALC and ALCO @ with transitive roles, role inclusions, inverse roles, role intersection, and/or functionality restrictions, are definitorially complete.