Conclusion

Combining the results from [De 95] and [Tob00] with the results from this paper, we obtain the classification of the complexity of concept satisfiability and TBox-consistency for various DLs and for TBoxes consisting either of cardinality restrictions or of general concept inclusion axioms shown in Figure 4, where we assume unary coding of numbers.

The result for
shows that the current efforts of extending very
expressive DLs as the logic
[HST99] and
[CDGL^{+}98b] or
propositional dynamic logics as
[DL96] with
nominals are difficult tasks, if one wants to obtain a practical decision
procedure, since already concept satisfiability for these logics is a
-hard problem.

We have shown that, while having the same complexity as , does not reach its expressive power [Tob99]. Cardinality restrictions, although interesting for knowledge representation, are inherently hard to handle algorithmically. The same applies to nominals in the presence of inverse roles and number restrictions. As an explanation for this we offer the lack of a tree model property, which was identified in [Var97] as an explanation for good algorithmic behaviour of many modal logics.

At a first glance, our results make
with cardinality restrictions on
concepts or
with general axioms obsolete for knowledge representation
because
delivers more expressive power at the same computational price.
Yet, is is likely that a dedicated algorithm for
may have better
average complexity than the
algorithm; such an algorithm has yet to be
developed. This is highly desirable as it would also be applicable to
reasoning problems for expressive DLs with nominals, which have applications
in the area of reasoning with database
schemata [CDL^{+}98,CDGL98a].

An interesting question lies in the coding of numbers: If we allow binary coding of numbers, the translation approach together with the result from [PST97] leads to a 2- algorithm. As for , it is an open question whether this additional exponential blow-up is necessary. A positive answer would settle the same question for while a proof of the negative answer might give hints how the result for might be improved. For with cardinality restrictions, we have partially solved this problem: with unary coding, the problem is -complete whereas, for binary coding, it is -hard.

May 02 2000