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
.