next up previous
Next: Internalisation of Axioms Up: ALCQIO Previous: ALCQIO

Unique Name Assumption

It should be noted that our definition of nominals is non-standard for Description Logics in the sense that we do not impose the unique name assumption that is widely made, i.e., for any two individual names $o_1,o_2
\in N_I$, $o_1^\mathcal{I}\neq o_2^\mathcal{I}$ is required. Even without a unique name assumption, it is possible to enforce distinct interpretation of nominals by adding axioms of the form $o_1 \sqsubseteq \neg o_2$. Moreover, imposing a unique name assumption in the presence of inverse roles and number restriction leads to peculiar effects. Consider the following \ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Box}}:

\begin{displaymath}T = \{ o \sqsubseteq \ensuremath{(\leqslant k \; R \; \top)} , \ \top \sqsubseteq \exists R^- . o \}
\end{displaymath}

Under the unique name assumption, T is consistent iff NI contains at most k individual names, because each individual name must be interpreted by a unique element of the domain, every element of the domain must be reachable from $o^\mathcal{I}$ via the role R, and $o^\mathcal{I}$ may have at most k R-successors. We believe that this dependency of the consistency of a \ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Box}} on constraints that are not explicit in the \ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Box}} is counter-intuitive and hence have not imposed the unique name assumption.

Nevertheless, it is possible to obtain a tight complexity bound for consistency of \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}- \ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Boxes}} with the unique name assumption without using Theorem 4.5, but by an immediate adaption of the proof of Theorem 3.8.

Corollary 4.10
Consistency of \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}- \ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Boxes}} with the unique name assumption is \textsc{NExp\-Time}-complete if unary coding of numbers assumed.

Proof. A simple inspection of the reduction used to prove Theorem 3.8, and especially of the proof of Lemma 3.6 shows that only a single nominal, which marks the upper right corner of the torus, is necessary to perform the reduction. If o is an individual name and $\textit{create}$ is a role name, then the following \ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Box}} defines a torus of exponential size:

\begin{displaymath}\begin{array}{r@{\;}c@{\;}ll}
T_n & = \bigl \{ & \top \sqsub...
...\xspace\sqcap D_{\textit{north}}\xspace\ \bigr \}
\end{array} \end{displaymath}

Since this reduction uses only a single individual name, the unique name assumption is irrelevant.


next up previous
Next: Internalisation of Axioms Up: ALCQIO Previous: ALCQIO

Stephan Tobies
May 02 2000