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 C_{T} 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 C_{T} is a reduction from consistency of - to -concept satisfiability. From Corollary 4.9 we know that the former problem is -complete. Obviously, C_{T} can be computed from T in polynomial time. Hence, the lower complexity bound transfers.