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,

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.

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

May 02 2000