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.
Assuming unary coding of numbers, the translation of a T is obviously computable in polynomial time.
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 .
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 - .