Next: Conclusion Up: ALCQIO Previous: Unique Name Assumption

#### Internalisation of Axioms

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.

Definition 4.11   Let T be an - . W.l.o.g., we assume that T is of the form . Let denote a fresh role name and i a fresh individual name. We define the function inductively on the structure of concepts by setting for all , for all , , , and . The internalisation CT of T is defined as follows:

Lemma 4.12
Let T be an - . T is consistent iff CT is satisfiable.

Proof. For the if-direction let be a model of CT with . This implies . Let be defined by

and .

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

where the equivalence (*) holds because of set equality and the definition of .

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 .

Again, the equivalence (*) holds due to set equality and the definition of . Since, for every , we have , Claim 2 yields that and hence

As a consequence, we obtain the sharper result that already pure concept satisfiability for is a -complete problem.

Corollary 4.13
Concept satisfiability for is -complete.

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.

Next: Conclusion Up: ALCQIO Previous: Unique Name Assumption

Stephan Tobies
May 02 2000