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 .