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 $\{ \top \sqsubseteq C_1, \dots, \top \sqsubseteq C_k \}$. Let $\textit{spy}$ denote a fresh role name and i a fresh individual name. We define the function $\cdot^{\textit{spy}}$ inductively on the structure of concepts by setting $A^{\textit{spy}} = A$ for all $A \in N_C$, $o^{\textit{spy}} = o$ for all $o \in N_I$, $(\neg C)^{\textit{spy}} = \neg C^{\textit{spy}}$, $(C_1 \sqcap C_2)^{\textit{spy}} = C_1^{\textit{spy}} \sqcap C_2^{\textit{spy}}$, and ${\ensuremath{(\geqslant n \; R \; C)} }^{\textit{spy}} = \ensuremath{(\geqslant n \; R \; (\exists {\textit{spy}^-}.i) \sqcap C^{\textit{spy}})}$. The internalisation C_T of T is defined as follows:

$$C_T = i \sqcap \underset{\top \sqsubseteq C \in T}{{\raisebox... ...\bigsqcup$\end{turn}}}}\forall \textit{spy}. C^{\textit{spy}}$$

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

Proof. For the if-direction let $\mathcal{I}$ be a model of C_T with $a \in (C_T)^\mathcal{I}$. This implies $i^\mathcal{I}= \{ a\}$. Let $\mathcal{I}'$ be defined by

$$\Delta^{\mathcal{I}'} = \{ a\} \cup \{ x \in \Delta^\mathcal{I}\mid (a,x) \in \textit{spy}^\mathcal{I} \}$$

and $\cdot^{\mathcal{I}'} = \cdot^\mathcal{I}\vert _{\Delta^{\mathcal{I}'}}$.

For every $x \in \Delta^{\mathcal{I}'}$ and every -concept C, we have $x \in (C^{\textit{spy}})^\mathcal{I}$ iff $x \in C^{\mathcal{I}'}$.

We proof this claim by induction on the structure of C. The only interesting case is $C = \ensuremath{(\geqslant n \; R \; D)}$. In this case $C^{\textit{spy}} = \ensuremath{(\geqslant n \; R \; (\exists {\textit{spy}^-}.i) \sqcap D^{\textit{spy}})}$. We have

$$\begin{align*}& x \in \ensuremath{(\geqslant n \; R \; (\exists {\textit{spy}^-}... ... \; & x \in \ensuremath{(\geqslant n \; R \; D)} ^{\mathcal{I}'} , \end{align*}$$

where the equivalence (*) holds because of set equality and the definition of $\mathcal{I}'$.

By construction, for every $\top \sqsubseteq C \in T$ and every $x \in \Delta^{\mathcal{I}'}$, $x \in (C^{\textit{spy}})^\mathcal{I}$. Due to Claim 1, this implies $x \in C^{\mathcal{I}'}$ and hence $\mathcal{I}' \models \top \sqsubseteq C$. For the only-if-direction, let $\mathcal{I}$ be an interpretation with $\mathcal{I}\models T$. We pick an arbitrary element $a \in \Delta^\mathcal{I}$ and define an extension $\mathcal{I}'$ of $\mathcal{I}$ by setting $i^{\mathcal{I}'} = \{ a \}$ and $\textit{spy}^{\mathcal{I}'} = \{ (a,x) \mid x \in \Delta^\mathcal{I}$. Since i and $\textit{spy}$ do not occur in T, we still have that $\mathcal{I}' \models T$.

For every $x \in \Delta^{\mathcal{I}'}$ and every -concept C that does not contain i or $\textit{spy}$, $x \in C^{\mathcal{I}'}$ iff $x \in (C^{\textit{spy}})^{\mathcal{I}'}$.

Again, this claim is proved by induction on the structure of concepts and the only interesting case is $C = \ensuremath{(\geqslant n \; R \; D)}$.

$$\begin{align*}& x \in \ensuremath{(\geqslant n \; R \; D)} ^{\mathcal{I}'}\\ \... ...s {\textit{spy}^-}.i) \sqcap D^{\textit{spy}})} ^{\mathcal{I}'} . \end{align*}$$

Again, the equivalence (*) holds due to set equality and the definition of $\mathcal{I}'$. Since, for every $\top \sqsubseteq C \in T$, we have $\mathcal{I}' \models \top \sqsubseteq C$, Claim 2 yields that $({{\raisebox{1.3ex}{\begin{turn}{180}$\bigsqcup$\end{turn}}}}_{\top \sqsubseteq C \in T} C^{\textit{spy}} )^{\mathcal{I}'} = \Delta^{\mathcal{I}'}$ and hence $a \in (C_T)^{\mathcal{I}'}$

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 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.