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.

**Figure 4:** Complexity of the reasoning problems
$\begin{figure}\begin{center} \framebox[\textwidth]{ \begin{tabular}{l\vert cc\... ...ce-c. & \textsc{NExp\-Time}\xspace-c. \end{tabular} } \end{center} \end{figure}$

The result for $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}$ shows that the current efforts of extending very expressive DLs as the logic $\mathcal{S\!H\!I\!Q}$ [HST99] and $\mathcal{D\!L\!R}$ [CDGL⁺98b] or propositional dynamic logics as $\mathsf{CPDL}_g$ [DL96] with nominals are difficult tasks, if one wants to obtain a practical decision procedure, since already concept satisfiability for these logics is a $\textsc{NExp\-Time}$ -hard problem.

We have shown that, while having the same complexity as $\ensuremath{C^2}$ , $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}$ 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 $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}$ with cardinality restrictions on concepts or $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}$ with general axioms obsolete for knowledge representation because $\ensuremath{C^2}$ delivers more expressive power at the same computational price. Yet, is is likely that a dedicated algorithm for $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}$ may have better average complexity than the $\ensuremath{C^2}$ 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- $\textsc{NExp\-Time}$ algorithm. As for $\ensuremath{C^2}$ , it is an open question whether this additional exponential blow-up is necessary. A positive answer would settle the same question for $\ensuremath{C^2}$ while a proof of the negative answer might give hints how the result for $\ensuremath{C^2}$ might be improved. For $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}$ with cardinality restrictions, we have partially solved this problem: with unary coding, the problem is $\textsc{Exp\-Time}$ -complete whereas, for binary coding, it is $\textsc{NExp\-Time}$ -hard.