Next: Complexity Results Up: Reasoning with Nominals Previous: Reasoning with Nominals

## Expressing Cardinality Restrictions Using Nominals

In the following we show how, under the assumption of unary coding of numbers, consistency of - can be polynomially reduced to consistency of - . It should be noted that, conversely, it is also possible to polynomially reduce consistency of - to consistency of - : for an arbitrary concept C, the cardinality restrictions force the interpretation of Cto be a singleton. Since we do not gain any further insight from this reduction, we do not formally prove this result.

Definition 4.3   Let be an - . W.l.o.g., we assume that T contains no cardinality restriction of the form as these are trivially satisfied by any interpretation. The translation of T, denoted by , is the - defined as follows:

where is defined depending on whether or .

where are fresh and distinct nominals and we use the convention that the empty disjunction is interpreted as to deal with the case ni = 0.

Assuming unary coding of numbers, the translation of a T is obviously computable in polynomial time.

Lemma 4.4
Let T be an - . T is consistent iff is consistent.

Proof. Let be a consistent . Hence, there is a model of T, and for each . We show how to construct a model of from . will be identical to in every respect except for the interpretation of the nominals oij (which do not appear in T). If , then implies . If ni = 0, then we have not introduced new nominals, and contains . Otherwise, we define such that . This implies and hence, in either case, . If , then ni > 0 must hold, and implies . Let be ni distinct elements from with . We set . Since we have chosen distinct individuals to interpret different nominals, we have for every . Moreover, implies and hence . We have chosen distinct nominals for every cardinality restrictions, hence the previous construction is well-defined and, since satisfies for every i, . For the converse direction, let be a models of . The fact that (and hence the consistency of T) can be shown as follows: let be an arbitrary cardinality restriction in T. If and ni = 0, then we have and, since , we have and hence . If and ni > 0, we have . From follows . If , then we have . From the first set of axioms we get . From the second set of axioms we get that, for every , . This implies that .

Theorem 4.5
Assuming unary coding of numbers, consistency of - can be polynomially reduced to consistency of - . Similarly, consistency of - can be polynomially reduced to consistency of - .

Proof. The first proposition follows from the fact that is polynomially computable from T if we assume unary coding of numbers and from Lemma 4.4. The second proposition follows from the fact that the translation does not introduce additional inverse roles. If T does not contain inverse roles, then neither does , and hence the result of translating an - is an - .

Next: Complexity Results Up: Reasoning with Nominals Previous: Reasoning with Nominals

Stephan Tobies
May 02 2000