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.
For the if-direction let
be a model of CT with
be defined by
-concept C, we have
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.