Conversely, using Theorem 4.5 enables us to transfer the -completeness result from Theorem 3.8 to .

**Proof. **
For
,
this is an immediate corollary of
Theorem 4.5 and
Theorem 3.8. Reasoning with
is as hard as
for
in the presences of nominals.

This results explains a gap in [De 95]. There the author establishes the complexity of satisfiability of knowledge bases consisting of and ABoxes both for , which allows for qualifying number restrictions, and for , which allows for inverse roles, by reduction to an -complete PDL. No results are given for the combination , which is a strict extension of . Corollary 4.8 shows that, assuming , there cannot be a polynomial reduction from the satisfiability problem of knowledge bases to an -complete PDL. Again, a possible explanation for this leap in complexity is the loss of the tree model property. While for and , consistency is decided by searching for a tree-like pseudo-models even in the presence of nominals, this seems no longer to be possible in the case of knowledge bases for .

May 02 2000