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 $\{(\leqslant 1 \; C), (\geqslant 1 \; C) \}$ 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 $T = \{ (\bowtie_1 n_1 \; C_1), \dots (\bowtie_k n_k \; C_k) \}$ be an - . W.l.o.g., we assume that T contains no cardinality restriction of the form $(\geqslant 0 \; C)$ as these are trivially satisfied by any interpretation. The translation of T, denoted by $\Phi(T)$, is the - defined as follows:

$$\Phi(T) = \bigcup \{ \Phi(\bowtie_i n_i \; C_i) \mid 1 \leq i \leq k \} ,$$

where $\Phi(\bowtie_i n_i \; C_i)$ is defined depending on whether $\bowtie_i = \leqslant$ or $\bowtie_i = \geqslant$.

$$\Phi(\bowtie_i n_i \; C_i) = \begin{cases} \{ C_i \sqsubse... ...eq n_i \} & \text{if } \bowtie_i = \geqslant \end{cases} ,$$

where $o_i^1, \dots, o_i^{n_i}$ are fresh and distinct nominals and we use the convention that the empty disjunction is interpreted as $\neg \top$ to deal with the case n_i = 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 $\Phi(T)$ is consistent.

Proof. Let $T = \{ (\bowtie_1 n_1 \; C_1), \dots (\bowtie_k n_k \; C_k) \}$ be a consistent . Hence, there is a model $\mathcal{I}$ of T, and $\mathcal{I}\models (\bowtie_i n_i \; C_i)$ for each $1 \leq i \leq k$. We show how to construct a model $\mathcal{I}'$ of $\Phi(T)$ from $\mathcal{I}$. $\mathcal{I}'$ will be identical to $\mathcal{I}$ in every respect except for the interpretation of the nominals o_i^j (which do not appear in T). If $\bowtie_i = \leqslant$, then $\mathcal{I}\models T$ implies $\sharp C_i^\mathcal{I}\leq n_i$. If n_i = 0, then we have not introduced new nominals, and $\Phi(T)$ contains $C_i \sqsubseteq \neg \top$. Otherwise, we define $(o_i^j)^{\mathcal{I}'}$ such that $C_i^\mathcal{I}\subseteq \{ (o_i^j)^{\mathcal{I}'} \mid 1 \leq j \leq n_i \}$. This implies $C_i^{\mathcal{I}'} \subseteq (o_i^1)^{\mathcal{I}'} \cup \dots \cup (o_i^{n_i})^{\mathcal{I}'}$ and hence, in either case, $\mathcal{I}' \models \Phi(\leqslant n_i \; C_i)$. If $\bowtie_i = \geqslant$, then n_i > 0 must hold, and $\mathcal{I}\models T$ implies $\sharp C_i^\mathcal{I}\geq n_i$. Let $x_1, \dots x_{n_i}$ be n_i distinct elements from $\Delta^\mathcal{I}$ with $\{ x_1, \dots, x_{n_i} \} \subseteq C_i^\mathcal{I}$. We set $(o_i^j)^{\mathcal{I}'} = \{x_j \}$. Since we have chosen distinct individuals to interpret different nominals, we have $\mathcal{I}' \models o_i^j \sqsubseteq \neg o_i^\ell$ for every $1 \leq i < \ell \leq n_i$. Moreover, $x_j \in C_i^\mathcal{I}$ implies $\mathcal{I}' \models o_i^j \sqsubseteq C_i$ and hence $\mathcal{I}' \models \Phi(\geqslant n_i \; C_i)$. We have chosen distinct nominals for every cardinality restrictions, hence the previous construction is well-defined and, since $\mathcal{I}'$ satisfies $\Phi(\bowtie_i n_i \; C_i)$ for every i, $\mathcal{I}' \models \Phi(T)$. For the converse direction, let $\mathcal{I}$ be a models of $\Phi(T)$. The fact that $\mathcal{I}\models T$ (and hence the consistency of T) can be shown as follows: let $(\bowtie_i n_i \; C_i)$ be an arbitrary cardinality restriction in T. If $\bowtie_i = \leqslant$ and n_i = 0, then we have $\Phi(\leqslant 0 \; C_i) = \{ C_i \sqsubseteq \; \neg \top \}$ and, since $\mathcal{I}\models \Phi(T)$, we have $C_i^\mathcal{I}= \emptyset$ and hence $\mathcal{I}\models (\leqslant 0 \; C_i)$. If $\bowtie_i = \leqslant$ and n_i > 0, we have $\{ C_i \sqsubseteq o_i^1 \sqcup \dots \sqcup o_i^{n_i} \} \subseteq \Phi(T)$. From $\mathcal{I}\models \Phi(T)$ follows $\sharp C_i^\mathcal{I}\leq \sharp (o_i^1 \sqcup \dots \sqcup o_i^{n_i})^\mathcal{I}\leq n_i$. If $\bowtie_i = \geqslant$, then we have $\{ o_i^j \sqsubseteq C_i \mid 1 \leq j \leq n_i \} \cup \{ o_i^j \sqsubseteq \neg o_i^\ell \mid 1 \leq j < \ell \leq n_i \} \subseteq \Phi(T)$. From the first set of axioms we get $\{ (o_i^j)^\mathcal{I}\mid 1 \leq j \leq n_i \} \subseteq C_i^\mathcal{I}$. From the second set of axioms we get that, for every $1 \leq j < \ell \leq n_i$, $(o_i^j)^\mathcal{I}\neq (o_i^\ell)^\mathcal{I}$. This implies that $n_i = \sharp \bigcup \{ (o_i^j)^\mathcal{I}\mid 1 \leq j \leq n_i \} \leq \sharp C_i^\mathcal{I}$.

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 $\Phi(T)$ 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 $\Phi(T)$, and hence the result of translating an - is an - .