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 , is required. Even without a unique name assumption, it is possible to enforce distinct interpretation of nominals by adding axioms of the form . Moreover, imposing a unique name assumption in the presence of inverse roles and number restriction leads to peculiar effects. Consider the following :

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 via the role R, and 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 is a role name, then the following defines a torus of exponential size:

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

Next: Internalisation of Axioms Up: ALCQIO Previous: ALCQIO

Stephan Tobies
May 02 2000