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 :

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

Under the unique name assumption, T is consistent iff N_I 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 on constraints that are not explicit in the 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 - 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 - with the unique name assumption is -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 defines a torus of exponential size:

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

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