In the presence of inverse roles and nominals, it is possible to internalise general inclusion axioms into concepts using the spy-point technique used, e.g., in [BS96,ABM99]. The main idea of this technique is to enforce that all elements in the model of a concept are reachable from a distinct point (the spy-point) marked by an individual name in a single step.
Proof.
For the if-direction let
be a model of CT with
.
This implies
.
Let
be defined by
For every
and every
-concept C, we have
iff
.
We proof this claim by induction on the structure of C. The only
interesting case is
.
In this case
.
We have
By construction, for every
and
every
,
.
Due to Claim 1, this
implies
and hence
.
For the only-if-direction, let
be an interpretation with
.
We pick an arbitrary element
and define an
extension
of
by setting
and
.
Since i and
do not occur in T, we
still have that
.
For every
and every
-concept C that does not contain i or
,
iff
.
Again, this claim is proved by induction on the structure of concepts and the
only interesting case is
.
As a consequence, we obtain the sharper result that already pure concept
satisfiability for
is a
-complete problem.
Proof.
From Lemma 4.12, we get that the function mapping a
-
T to CT is a reduction from consistency of
-
to
-concept satisfiability. From
Corollary 4.9 we know that the former problem
is
-complete. Obviously, CT can be computed from T in
polynomial time. Hence, the lower complexity bound transfers.