${\sf X}$, if
$(a_{0},{m\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha}})\in
G^{\mathcal{I}}$ then $\mathcal{O}\models(C\sqsubseteq G,m)$. Since $D$ is
either a concept name or is of the form $\exists P.\top$ (by the form of
${\cal E\\!LHI}_{\bot}$ GCIs and assumption that $D\neq\bot$) and
$\mathcal{O}\not\models(C\sqsubseteq D,m_{0})$, it follows that
$(a_{0},{m_{0}\times\Pi_{(\alpha,v^{i}_{\alpha})\in\mathcal{A}_{C}}v^{i}_{\alpha}})\notin
D^{\mathcal{I}}$. ∎

Regarding role inclusions, the following proposition can be proven.

######  Proposition B.4.

$\mathcal{O}\models(P_{1}\sqsubseteq P_{2},m)$ iff
$\mathcal{O}\cup\\{(P_{1}(a_{0},b_{0}),1)\\}\models(P_{2}(a_{0},b_{0}),m)$
where $a_{0},b_{0}$ are fresh individual names.

Let $\mathcal{O}$ be a consistent $\sf{Why}[{\sf X}]$-annotated ${\cal
E\\!LHI}_{\bot}$ ontology in normal form, and let $B(a_{0})$ be a concept
assertion and $m_{0}$ be a monomial over ${\sf X}$. For all
$a,b\in\mathsf{ind}(\mathcal{O})$ and $R\in{\sf N_{R}}$, assume that the
concept or role names $C_{a},R_{ab}$ do not occur in $\mathcal{O}$ and let

$\displaystyle\mathcal{T}_{C_{a}}=$ $\displaystyle\\{(C_{a}\sqsubseteq
A,v)\mid(A(a),v)\in\mathcal{O}\\}\ \cup$ $\displaystyle\\{(R_{ab}\sqsubseteq
R,v),(C_{a}\equiv\exists R_{ab},1),(C_{b}\equiv\exists
R_{ab}^{-},1)\mid(R(a,b),v)\in\mathcal{O}\\}$ $\displaystyle\mathcal{T}=$
$\displaystyle\bigcup_{a\in\mathsf{ind}(\mathcal{O})}\mathcal{T}_{C_{a}}\cup(\mathcal{O}\setminus\\{(\alpha,v)\mid\alpha\text{
is an assertion}\\}).$

$\mathcal{T}$ can be computed in polynomial time. We will use the following
lemma to show that $\mathcal{O}\models(B(a_{0}),m_{0})$ iff
$\mathcal{T}\models(C_{a_{0}}\sqsubseteq B,m_{0})$ or
$\mathcal{T}\models(\top\sqsubseteq B,m_{0})$.

######  Lemma B.5.

There exists a model $\mathcal{I}$ of $\mathcal{T}$ such that

  1. 1.

for every $a\in\mathsf{ind}(\mathcal{O})$, $a^{\mathcal{I}}=a$ and
$C_{a}^{\mathcal{I}}=\\{(a^{\mathcal{I}},1)\\}$,

  2. 2.

for every $(R(a,b),v)\in\mathcal{O}$,
$R_{ab}^{\mathcal{I}}=\\{(a^{\mathcal{I}},b^{\mathcal{I}},1)\\}$, and

  3. 3.

for every $a\in\mathsf{ind}(\mathcal{O})$ and $A\in{\sf N_{C}}$ that occurs in
$\mathcal{O}$, if $(a^{\mathcal{I}},m)\in A^{\mathcal{I}}$ then
$\mathcal{T}\models(C_{a}\sqsubseteq A,m)$ or
$\mathcal{T}\models(\top\sqsubseteq A,m)$.

Moreover, $\mathcal{I}$ is a model of $\mathcal{O}$.

###### Proof.

Let $\epsilon\notin\mathsf{ind}(\mathcal{O})$. We inductively build an
interpretation $\mathcal{I}=\bigcup_{i\geq 0}\mathcal{I}_{i}$ such that for
every $i$, $\mathcal{I}_{i}$ fulfills conditions (1)-(2) of the lemma and the
following stronger version of condition (3): for every
$a\in\mathsf{ind}(\mathcal{O})$, concept name $A$ and role $P:=R\mid R^{-}$
that occur in $\mathcal{O}$,

  * •

if $(a^{\mathcal{I}_{i}},m)\in A^{\mathcal{I}_{i}}$, then
$\mathcal{T}\models(C_{a}\sqsubseteq A,m)$ or
$\mathcal{T}\models(\top\sqsubseteq A,m)$,

  * •

if $(a^{\mathcal{I}_{i}},m)\in(\exists P.A)^{\mathcal{I}_{i}}$, then
$\mathcal{T}\models(C_{a}\sqsubseteq\exists P^{\prime},n_{1})$ or
$\mathcal{T}\models(\top\sqsubseteq\exists P^{\prime},n_{1})$,
$\mathcal{T}\models(P^{\prime}\sqsubseteq P,n_{2})$, and (i) if $A=\top$, then
$m={n_{1}\times n_{2}}$, and (ii) if $A\neq\top$, then
$\mathcal{T}\models(\exists\mathsf{inv}(P^{\prime})\sqsubseteq A,n_{3})$ with
$m={n_{1}\times n_{2}\times n_{3}}$.

We start with
$\Delta^{\mathcal{I}_{0}}=\mathsf{ind}(\mathcal{O})\cup\\{\epsilon\\}$,
$a^{\mathcal{I}_{0}}=\epsilon$ for every $a\in{\sf
N_{I}}\setminus\mathsf{ind}(\mathcal{O})$. Also, for every
$a\in\mathsf{ind}(\mathcal{O})$, $a^{\mathcal{I}_{0}}=a$ and
$C_{a}^{\mathcal{I}_{0}}=\\{(a,1)\\}$; and
$R_{ab}^{\mathcal{I}_{0}}=\\{(a,b,1)\\}$ for every $(R(a,b),v)\in\mathcal{O}$.
By construction, $\mathcal{I}_{0}$ fulfills conditions (1)-(2) of the lemma,
as well as the stronger version of condition (3). Indeed, for every $A$ and
$P$ that occur in $\mathcal{O}$, $A^{\mathcal{I}_{0}}=(\exists
P.A)^{\mathcal{I}_{0}}=\emptyset$.

To build $\mathcal{I}_{i+1}$ from $\mathcal{I}_{i}$, we apply the following
rules. For each rule, we show that if $\mathcal{I}_{i}$ fulfills our
requirements, then it is also the case of $\mathcal{I}_{i+1}$.

  1. 1.

If $(P_{1}\sqsubseteq P_{2},v)\in\mathcal{T}$ and $(d,f,m)\in
P_{1}^{\mathcal{I}_{i}}$, then
$P_{2}^{\mathcal{I}_{i+1}}=P_{2}^{\mathcal{I}_{i}}\cup\\{(d,f,{v\times
m})\\}$.
Assume that $\mathcal{I}_{i}$ fulfills our requirements. The interpretation of
the individual names and concept and role names of the form $C_{a}$ and
$R_{ab}$ is not modified (since $P_{2}$ cannot be of the form $R_{ab}$ by the
form of the RIs in $\mathcal{T}$) so conditions (1) and (2) still hold. We
show that it is also the case of the last condition.

If $d=a^{\mathcal{I}_{i}}$ for some $a\in\mathsf{ind}(\mathcal{O})$ and
$(d,n)\in(\exists P_{2}.A)^{\mathcal{I}_{i+1}}$ while $(d,n)\notin(\exists
P_{2}.A)^{\mathcal{I}_{i}}$, there must be some $(f,o)\in A^{\mathcal{I}_{i}}$
such that $n={v\times m\times o}$ (note that if $A=\top$, then $o=1$). It
follows that $(d,{m\times o})\in(\exists P_{1}.A)^{\mathcal{I}_{i}}$ so since
$\mathcal{I}_{i}$ fulfills the requirements, it holds that
$\mathcal{T}\models(C_{a}\sqsubseteq\exists P_{1}^{\prime},n_{1})$ or
$\mathcal{T}\models(\top\sqsubseteq\exists P_{1}^{\prime},n_{1})$,
$\mathcal{T}\models(P_{1}^{\prime}\sqsubseteq P_{1},n_{2})$ and (i) if
$A=\top$, then ${m\times o}={n_{1}\times n_{2}}$ and (ii) if $A\neq\top$, then
$\mathcal{T}\models(\exists\mathsf{inv}(P_{1}^{\prime})\sqsubseteq A,n_{3})$
with ${m\times o}={n_{1}\times n_{2}\times n_{3}}$. Since $(P_{1}\sqsubseteq
P_{2},v)\in\mathcal{T}$ , it thus follows that
$\mathcal{T}\models(P_{1}^{\prime}\sqsubseteq P_{2},v\times n_{2})$ thus the
condition holds (since if $A=\top$, $n={v\times m\times o}={n_{1}\times
v\times n_{2}}$ and if $A\neq\top$, $n={v\times m\times o}={n_{1}\times
v\times n_{2}\times n_{3}}$).

In a similar way, if $f=a^{\mathcal{I}_{i}}$ for some
$a\in\mathsf{ind}(\mathcal{O})$ and
$(f,n)\in(\exists\mathsf{inv}(P_{2}).A)^{\mathcal{I}_{i+1}}$ while
$(f,n)\notin(\exists\mathsf{inv}(P_{2}).A)^{\mathcal{I}_{i}}$, there must be
some $(d,o)\in A^{\mathcal{I}_{i}}$ such that $n={v\times m\times o}$. We can
show analogously that the property holds.

  2. 2.

If $(A\sqsubseteq B,v)\in\mathcal{T}$ and $(d,m)\in A^{\mathcal{I}_{i}}$, then
$B^{\mathcal{I}_{i+1}}=B^{\mathcal{I}_{i}}\cup\\{(d,{v\times m})\\}$.
It is easy to check that if $\mathcal{I}_{i}$ fulfills our requirements, then
it is also the case of $\mathcal{I}_{i+1}$. In particular, note that by
construction of $\mathcal{T}$, $B$ is not of the form $C_{a}$.

  3. 3.

If $(A_{1}\sqcap A_{2}\sqsubseteq B,v)\in\mathcal{T}$ and $(d,m_{1})\in
A_{1}^{\mathcal{I}_{i}}$, $(d,m_{2})\in A_{2}^{\mathcal{I}_{i}}$ then
$B^{\mathcal{I}_{i+1}}=B^{\mathcal{I}_{i}}\cup\\{(d,{v\times m_{1}\times
m_{2}})\\}$.
It is easy to check that if $\mathcal{I}_{i}$ fulfills our requirements, then
it is also the case of $\mathcal{I}_{i+1}$. In particular, note that by
construction of $\mathcal{T}$, $B$ is not of the form $C_{a}$. We detail the
proof that the first point of the stronger version of condition (3) holds (the
second point is similar). If $d=a^{\mathcal{I}_{i}}$ for some
$a\in\mathsf{ind}(\mathcal{O})$, since $(d,m_{1})\in A_{1}^{\mathcal{I}_{i}}$,
$(d,m_{2})\in A_{1}^{\mathcal{I}_{i}}$ and $\mathcal{I}_{i}$ fulfills the
requirements, then (1) $\mathcal{T}\models(C_{a}\sqsubseteq A_{1},m_{1})$ or
(2) $\mathcal{T}\models(\top\sqsubseteq A_{1},m_{1})$, and (i)
$\mathcal{T}\models(C_{a}\sqsubseteq A_{1},m_{2})$ or (ii)
$\mathcal{T}\models(\top\sqsubseteq A_{1},m_{2})$. In case (1)-(i), since
$(A_{1}\sqcap A_{2}\sqsubseteq B,v)\in\mathcal{T}$, it is easy to check that
$\mathcal{T}\models(C_{a}\sqsubseteq B,{v\times m_{1}\times m_{2}})$. In case
(2)-(ii), in the same way, $\mathcal{T}\models(\top\sqsubseteq B,{v\times
m_{1}\times m_{2}})$. Finally in case (1)-(ii) (and (2)-(i) is similar), let
$\mathcal{J}$ be a model of $\mathcal{T}$ and $(e,n)\in C_{a}^{\mathcal{J}}$.
Since $\mathcal{T}\models(C_{a}\sqsubseteq A_{1},m_{1})$, $(e,n\times
m_{1})\in A_{1}^{\mathcal{J}}$, and since $\mathcal{T}\models(\top\sqsubseteq
A_{1},m_{2})$, $(e,m_{2})\in A_{2}^{\mathcal{J}}$. Hence $(e,n\times
m_{1}\times m_{2})\in(A_{1}\sqcap A_{2})^{\mathcal{J}}$, so $(e,n\times
m_{1}\times m_{2}\times v)\in B^{\mathcal{J}}$. It follows that
$\mathcal{T}\models(C_{a}\sqsubseteq B,m_{1}\times m_{2}\times v)$.

  4. 4.

If $(\exists P.A\sqsubseteq B,v)\in\mathcal{T}$ and $(d,f,m_{1})\in
P^{\mathcal{I}_{i}}$, $(f,m_{2})\in A^{\mathcal{I}_{i}}$, then
$B^{\mathcal{I}_{i+1}}=B^{\mathcal{I}_{i}}\cup\\{(d,{v\times m_{1}\times
m_{2}})\\}$.
It is easy to check that if $\mathcal{I}_{i}$ fulfills our requirements, then
it is also the case of $\mathcal{I}_{i+1}$. In particular, note that by
construction of $\mathcal{T}$, $B$ is not of the form $C_{a}$. We detail the
proof that the first point of the stronger version of condition (3) holds (the
second point is similar). If $d=a^{\mathcal{I}_{i}}$ for some
$a\in\mathsf{ind}(\mathcal{O})$, since $(d,{m_{1}\times m_{2}})\in(\exists
P.A)^{\mathcal{I}_{i}}$ and $\mathcal{I}_{i}$ fulfills the requirements, then
either (i) $\mathcal{T}\models(C_{a}\sqsubseteq\exists P^{\prime},n_{1})$ or
(ii) $\mathcal{T}\models(\top\sqsubseteq\exists P^{\prime},n_{1})$, and
$\mathcal{T}\models(P^{\prime}\sqsubseteq P,n_{2})$ and
$\mathcal{T}\models(\exists\mathsf{inv}(P^{\prime})\sqsubseteq A,n_{3})$ with
${m_{1}\times m_{2}}={n_{1}\times n_{2}\times n_{3}}$. It is easy to check
that it follows that in case (i) $\mathcal{T}\models(C_{a}\sqsubseteq
B,n_{1}\times n_{2}\times n_{3}\times v)$, i.e.
$\mathcal{T}\models(C_{a}\sqsubseteq B,{v\times m_{1}\times m_{2}})$ and in
case (ii) $\mathcal{T}\models(\top\sqsubseteq B,n_{1}\times n_{2}\times
n_{3}\times v)$, i.e. $\mathcal{T}\models(\top\sqsubseteq B,{v\times
m_{1}\times m_{2}})$.

  5. 5.

If $(A\sqsubseteq\exists P,v)\in\mathcal{T}$ and $(d,m)\in
A^{\mathcal{I}_{i}}$, then:

     * •

Case 1: $A$ is not of the form $C_{a}$. Set
$\Delta^{\mathcal{I}_{i+1}}=\Delta^{\mathcal{I}_{i}}\cup\\{f\\}$ where
$f\notin\Delta^{\mathcal{I}_{i}}$ and
$P^{\mathcal{I}_{i+1}}=P^{\mathcal{I}_{i}}\cup\\{(d,f,{v\times m})\\}$. It is
easy to check that if $\mathcal{I}_{i}$ fulfills the requirements, then so
does $\mathcal{I}_{i+1}$. Indeed, $P$ cannot be of the form $R_{ab}$ or
$R_{ab}^{-}$ by construction and there is no $a\in\mathsf{ind}(\mathcal{O})$
such that $a^{\mathcal{I}_{i}}=f$ so the only point to check is the second
point of the stronger version of condition (3). If $d=a^{\mathcal{I}_{i}}$ for
some $a\in\mathsf{ind}(\mathcal{O})$, and $(d,n)\in(\exists
P^{\prime}.C)^{\mathcal{I}_{i+1}}$ while $(d,n)\notin(\exists
P^{\prime}.C)^{\mathcal{I}_{i}}$, the only possibility is that $P^{\prime}=P$,
$C=\top$ and $n=v\times m$. Since $(a^{\mathcal{I}_{i}},m)\in
A^{\mathcal{I}_{i}}$ and $\mathcal{I}_{i}$ fulfills the requirements,
$\mathcal{T}\models(C_{a}\sqsubseteq A,m)$, so since $(A\sqsubseteq\exists
P,v)\in\mathcal{T}$, it is easy to check that
$\mathcal{T}\models(C_{a}\sqsubseteq\exists P,v\times m)$. Moreover
$\mathcal{T}\models(P\sqsubseteq P,1)$ trivially. Hence, the property holds.

     * •

Case 2: $A=C_{a}$. Since $C_{a}^{\mathcal{I}_{i}}=\\{(a,1)\\}$, then $d=a$ and
$v=1$. By construction of $\mathcal{T}$, either (i) there is
$(R(a,b),u)\in\mathcal{O}$ such that $\exists P=\exists R_{ab}$,
$R_{ab}^{\mathcal{I}_{i}}=\\{(a,b,1)\\}$ so $A^{\mathcal{I}_{i}}=\exists
P^{\mathcal{I}_{i}}$ or (ii) there is $(R(b,a),u)\in\mathcal{O}$ such that
$\exists P=\exists R_{ba}^{-}$, $R_{ba}^{\mathcal{I}_{i}}=\\{(b,a,1)\\}$ so
$A^{\mathcal{I}_{i}}=\exists P^{\mathcal{I}_{i}}$. Hence $(A\sqsubseteq\exists
P,v)$ is already satisfied in $\mathcal{I}_{i}$ and the rule does nothing.

Since $\mathcal{I}$ has been obtained by applying rules to satisfy all axioms
of $\mathcal{T}$ (as $\mathcal{T}$ is in normal form), $\mathcal{I}$ is a
model of $\mathcal{T}$ and since rule application preserves conditions (1) to
(3) of the lemma, $\mathcal{I}$ satisfies them.

Finally, we show that $\mathcal{I}$ is a model of the assertions of
$\mathcal{O}$, hence a model of $\mathcal{O}$. Let $(A(a),v)\in\mathcal{O}$.
Since $C_{a}^{\mathcal{I}}=\\{(a^{\mathcal{I}},1)\\}$,
$\mathcal{I}\models\mathcal{T}$ and $(C_{a}\sqsubseteq A,v)\in\mathcal{T}$,
then $(a^{\mathcal{I}},v)=(a^{\mathcal{I}},v)\in A^{\mathcal{I}}$. Let
$(R(a,b),v)\in\mathcal{O}$. Since
$R_{ab}^{\mathcal{I}}=\\{(a^{\mathcal{I}},b^{\mathcal{I}},1)\\}$,
$(R_{ab}\sqsubseteq R,v)\in\mathcal{T}$ and $\mathcal{I}\models\mathcal{T}$,
then $(a^{\mathcal{I}},b^{\mathcal{I}},v)\in R^{\mathcal{I}}$. This concludes
the proof of the lemma. ∎

######  Proposition B.6.

If $\mathcal{O}$ is consistent, $\mathcal{O}\models(B(a_{0}),m_{0})$ iff
$\mathcal{T}\models(C_{a_{0}}\sqsubseteq B,m_{0})$ or
$\mathcal{T}\models(\top\sqsubseteq B,m_{0})$.

###### Proof.

Assume that $\mathcal{T}\not\models(C_{a_{0}}\sqsubseteq B,m_{0})$ and
$\mathcal{T}\not\models(\top\sqsubseteq B,m_{0})$. By Lemma B.5, there exists
a model $\mathcal{I}$ of $\mathcal{O}$ such that
$(a_{0}^{\mathcal{I}},m_{0})\in B^{\mathcal{I}}$ implies
$\mathcal{T}\models(C_{a_{0}}\sqsubseteq B,m_{0})$ or
$\mathcal{T}\models(\top\sqsubseteq B,m_{0})$. It follows that
$(a_{0}^{\mathcal{I}},m_{0})\notin B^{\mathcal{I}}$, thus
$\mathcal{O}\not\models(B(a_{0}),m_{0})$.

In the other direction, assume that $\mathcal{O}\not\models(B(a_{0}),m_{0})$.
Assume for a contradiction that $\mathcal{T}\models(\top\sqsubseteq B,m_{0})$.
Then $\mathcal{O}\models(\top\sqsubseteq B,m_{0})$ by the form of the GCIs in
$\mathcal{T}\setminus\mathcal{O}$. It follows that
$\mathcal{O}\models(B(a),m_{0})$ for every $a\in\mathsf{ind}(\mathcal{O})$,
and in particular for $a_{0}$. Hence $\mathcal{T}\not\models(\top\sqsubseteq
B,m_{0})$. We next show that $\mathcal{T}\not\models(C_{a_{0}}\sqsubseteq
B,m_{0})$.

Let $\mathcal{I}$ be a model of $\mathcal{O}$ such that
$\mathcal{I}\not\models(B(a_{0}),m_{0})$, i.e.
$(a_{0}^{\mathcal{I}},m_{0})\notin B^{\mathcal{I}}$. Let $\mathcal{J}$ be the
interpretation that extends $\mathcal{I}$ with
$C_{a}^{\mathcal{J}}=\\{(a^{\mathcal{I}},1)\\}$ for every
$a\in\mathsf{ind}(\mathcal{O})$, and
$R_{ab}^{\mathcal{J}}=\\{(a^{\mathcal{I}},b^{\mathcal{I}},1)\\}$ for all
$a,b\in\mathsf{ind}(\mathcal{O})$ and every $R\in{\sf N_{R}}$. Since
$(a_{0}^{\mathcal{I}},1)\in C_{a_{0}}^{\mathcal{J}}$ and
$(a_{0}^{\mathcal{I}},m_{0})\notin B^{\mathcal{J}}$, then
$\mathcal{J}\not\models(C_{a_{0}}\sqsubseteq B,m_{0})$. We show that
$\mathcal{J}$ is a model of $\mathcal{T}$, so that
$\mathcal{T}\not\models(C_{a_{0}}\sqsubseteq B,m_{0})$. It is clear that
$\mathcal{J}$ is a model of all GCIs and RIs in $\mathcal{O}$ since
interpretations of concepts and roles that occur in $\mathcal{O}$ are not
modified. We now consider the different kinds of RIs and GCIs in
$\mathcal{T}\setminus\mathcal{O}$.

  * •

Let $(R_{ab}\sqsubseteq R,v)\in\mathcal{T}$. By construction of $\mathcal{J}$,
$R_{ab}^{\mathcal{J}}=\\{(a^{\mathcal{I}},b^{\mathcal{I}},1)\\}$ and since
$(R(a,b),v)\in\mathcal{O}$ and $\mathcal{I}$ is a model of $\mathcal{O}$, then
$(a^{\mathcal{I}},b^{\mathcal{I}},v)\in R^{\mathcal{J}}$. Thus
$\mathcal{J}\models(R_{ab}\sqsubseteq R,v)$.

  * •

Let $(C_{a}\sqsubseteq A,v)\in\mathcal{T}\setminus\mathcal{O}$ with $A\in{\sf
N_{C}}$. Since $(A(a),v)\in\mathcal{O}$ and $\mathcal{I}\models\mathcal{O}$,
then $(a^{\mathcal{I}},v)\in A^{\mathcal{J}}$. Thus, since
$C_{a}^{\mathcal{J}}=\\{(a^{\mathcal{I}},1)\\}$, it follows that
$\mathcal{J}\models(C_{a}\sqsubseteq A,v)$.

  * •

Let $(C_{a}\equiv\exists R_{ab},1)\in\mathcal{T}\setminus\mathcal{O}$. By
construction $C_{a}^{\mathcal{J}}=\\{(a^{\mathcal{I}},1)\\}$ and
$R_{ab}^{\mathcal{J}}=\\{(a^{\mathcal{I}},b^{\mathcal{I}},1)\\}$ so $(\exists
R_{ab})^{\mathcal{J}}=\\{(a^{\mathcal{I}},1)\\}$. Hence
$\mathcal{J}\models(C_{a}\equiv\exists R_{ab},1)$.

  * •

Let $(C_{b}\equiv\exists R_{ab}^{-},1)\in\mathcal{T}\setminus\mathcal{O}$. By
construction $C_{b}^{\mathcal{J}}=\\{(b^{\mathcal{I}},1)\\}$ and
$R_{ab}^{\mathcal{J}}=\\{(a^{\mathcal{I}},b^{\mathcal{I}},1)\\}$ so $(\exists
R_{ab}^{-})^{\mathcal{J}}=\\{(b^{\mathcal{I}},1)\\}$. Hence
$\mathcal{J}\models(C_{b}\sqsubseteq\exists R_{ab}^{-},1)$.

We conclude that $\mathcal{J}\models\mathcal{T}$, so
$\mathcal{T}\not\models(C_{a_{0}}\sqsubseteq B,m_{0})$. ∎

Regarding role assertions, we have the following proposition.

######  Proposition B.7.

If $\mathcal{O}$ is consistent, $\mathcal{O}\models(R(a_{0},b_{0}),m_{0})$ iff
$\mathcal{T}_{S_{a_{0},b_{0}}}\models(S\sqsubseteq R,m_{0})$ where $S$ is a
fresh role name and

$\displaystyle\mathcal{T}_{S_{a_{0},b_{0}}}=$ $\displaystyle\\{(S\sqsubseteq
R^{\prime},v)\mid(R^{\prime}(a_{0},b_{0}),v)\in\mathcal{O}\\}\ \cup$
$\displaystyle\\{(S\sqsubseteq
R^{\prime-},v)\mid(R^{\prime}(b_{0},a_{0}),v)\in\mathcal{O}\\}\ \cup$
$\displaystyle\\{(P_{1}\sqsubseteq P_{2},v)\mid(P_{1}\sqsubseteq
P_{2},v)\in\mathcal{O}\\}.$

###### Proof.

Assume that $\mathcal{O}\not\models(R(a_{0},b_{0}),m_{0})$ and let
$\mathcal{I}$ be a model of $\mathcal{O}$ such that
$\mathcal{I}\not\models(R(a_{0},b_{0}),m_{0})$. Let $\mathcal{J}$ the
interpretation that extends $\mathcal{I}$ with
$S^{\mathcal{J}}=\\{(a_{0}^{\mathcal{I}},b_{0}^{\mathcal{I}},1)\\}$. Since
$\mathcal{I}$ is a model of $\mathcal{O}$, it is easy to see that
$\mathcal{J}$ is a model of $\mathcal{T}_{S_{a_{0},b_{0}}}$ (in particular,
for every $(S\sqsubseteq R^{\prime},v)\in\mathcal{T}_{S_{a_{0},b_{0}}}$,
$(R^{\prime}(a_{0},b_{0}),v)\in\mathcal{O}$ so
$(a_{0}^{\mathcal{I}},b_{0}^{\mathcal{I}},v)\in R^{\prime\mathcal{J}}$, and
similarly for $(S\sqsubseteq R^{\prime-},v)\in\mathcal{T}_{S_{a_{0},b_{0}}}$).
Moreover, $\mathcal{J}\not\models(S\sqsubseteq R,m_{0})$ so
$\mathcal{T}_{S_{a_{0},b_{0}}}\not\models(S\sqsubseteq R,m_{0})$.

In the other direction, assume that
$\mathcal{O}\models(R(a_{0},b_{0}),m_{0})$. Let $\mathcal{I}_{\mathcal{O}}$ be
the canonical model of $\mathcal{O}$. By Theorem 3.14,
$\mathcal{I}_{\mathcal{O}}\models(R(a_{0},b_{0}),m_{0})$, i.e.
$(a_{0},b_{0},m_{0})\in R^{\mathcal{I}_{\mathcal{O}}}$. Since $a_{0}$ and
$b_{0}$ are individual names that occur in $\mathcal{O}$ (otherwise
$\mathcal{O}\not\models(R(a_{0},b_{0}),m_{0})$ trivially), it follows from the
construction of $\mathcal{I}_{\mathcal{O}}$ that there exist an assertion
$(R_{1}(a_{0},b_{0}),v)$ or $(R_{1}(b_{0},a_{0}),v)$ in $\mathcal{O}$, which
we denote $(P_{1}(a_{0},b_{0}),v)$ with $P_{1}=R_{1}$ in the former case and
$P_{1}=R_{1}^{-}$ in the latter, and a sequence of RIs
$(\alpha_{1},v_{1}),\dots,(\alpha_{n},v_{n})\in\mathcal{O}$ such that
$(a_{0},b_{0},m_{0})\in R^{\mathcal{I}_{\mathcal{O}}}$ results from the
application of this sequence of RIs to $(a_{0},b_{0},v)\in
P_{1}^{\mathcal{I}_{0}}$, so that $m_{0}=v\times\prod_{i=1}^{n}v_{i}$.

Let $\mathcal{J}$ be a model of $\mathcal{T}_{S_{a_{0},b_{0}}}$ and let
$(e,f,n)\in S^{\mathcal{J}}$. Since $\mathcal{J}\models(S\sqsubseteq
P_{1},v)$, $(e,f,n\times v)\in P_{1}^{\mathcal{J}}$. Then, since
$\mathcal{J}\models(\alpha_{i},v_{i})$ for every $1\leq i\leq n$, it is easy
to show that $(e,f,n\times v\times\prod_{i=1}^{n}v_{i})\in R^{\mathcal{J}}$,
i.e. $(e,f,n\times m_{0})\in R^{\mathcal{J}}$. It follows that
$\mathcal{J}\models(S\sqsubseteq R,m_{0})$, hence
$\mathcal{T}_{S_{a_{0},b_{0}}}\models(S\sqsubseteq R,m_{0})$. ∎

##### Proof of Theorem 4.7

Recall that $\mathsf{saturate}(\mathcal{O})$ is obtained by starting with

$\displaystyle\mathcal{S}:=\mathcal{O}$ $\displaystyle\cup\\{(\top(a),1)\mid
a\in\mathsf{ind}(\mathcal{O})\\}$ $\displaystyle\cup\\{(A\sqsubseteq A,1)\mid
A\in({\sf N_{C}}\cap\mathsf{sig}(\mathcal{O}))\cup\\{\top,\bot\\}\\}$
$\displaystyle\cup\\{(R\sqsubseteq R,1),(R^{-}\sqsubseteq R^{-},1),(\exists
R.\bot\sqsubseteq\bot,1),(\exists R^{-}.\bot\sqsubseteq\bot,1)\mid R\in{\sf
N_{R}}\cap\mathsf{sig}(\mathcal{O})\\}$
$\displaystyle\cup\\{(\mathsf{inv}(P_{1})\sqsubseteq\mathsf{inv}(P_{2}),m)\mid(P_{1}\sqsubseteq
P_{2},m)\in\mathcal{O}\\}$
$\displaystyle\cup\\{(\mathsf{inv}(P_{1})\sqcap\mathsf{inv}(P_{2})\sqsubseteq\bot,m)\mid(P_{1}\sqcap
P_{2}\sqsubseteq\bot,m)\in\mathcal{O}\\}$

and extending $\mathcal{S}$ through an iterative application of the rules from
Table 2 until no more rules are applicable.

For point (1) of Theorem 4.7, i.e. soundness of the completion algorithm, we
show the following stronger lemma.

######  Lemma B.8.

Let $\mathsf{saturate}(\mathcal{O})$ be the result of saturating
$\mathcal{O}$, $\alpha$ be an _assertion, GCI or RI_ and
$m\in\mathsf{mon}({\sf X})$. If $(\alpha,m)\in\mathsf{saturate}(\mathcal{O})$
then $\mathcal{O}\models(\alpha,m)$.

###### Proof.

If $\mathcal{O}$ is inconsistent, the lemma is trivial since
$\mathcal{O}\models(\alpha,m)$ for every $(\alpha,m)$. We thus assume that
$\mathcal{O}$ is consistent and show that for every model $\mathcal{I}$ of
$\mathcal{O}$, for every assertion, GCI, or RI $\alpha$ and every monomial
$m$, if $(\alpha,{m})\in\mathsf{saturate}(\mathcal{O})$ then
$\mathcal{I}\models(\alpha,{m})$.

Let $\mathcal{I}$ be a model of $\mathcal{O}$. The proof is by induction on
the number $i$ of completion steps that have been applied before adding
$(\alpha,{m})$ in $\mathsf{saturate}(\mathcal{O})$. For the base case $i=0$,
we have the following cases.

  * •

If $(\alpha,{m})\in\mathcal{O}$, since $\mathcal{I}$ is a model of
$\mathcal{O}$, $\mathcal{I}\models(\alpha,m)$.

  * •

If $(\alpha,{m})$ is of the form $(\top(a),1)$ for some
$a\in\mathsf{ind}(\mathcal{O})$, $(A\sqsubseteq A,1)$ for some $A\in({\sf
N_{C}}\cap\mathsf{sig}(\mathcal{O}))\cup\\{\top,\bot\\}$, $(R\sqsubseteq
R,1)$, $(R^{-}\sqsubseteq R^{-},1)$, $(\exists R.\bot\sqsubseteq\bot,1)$ or
$(\exists R^{-}.\bot\sqsubseteq\bot,1)$ for some $R\in{\sf
N_{R}}\cap\mathsf{sig}(\mathcal{O})$, $\mathcal{I}\models(\alpha,m)$ trivially
(recall that $\bot^{\mathcal{I}}=\emptyset$ and $(\exists
R^{(-)}.\bot)^{\mathcal{I}}=\emptyset$).

  * •

If $(\alpha,{m})$ is of the form
$(\mathsf{inv}(P_{1})\sqsubseteq\mathsf{inv}(P_{2}),m)$ for some
$(P_{1}\sqsubseteq P_{2},m)\in\mathcal{O}$, since $\mathcal{I}$ is a model of
$\mathcal{O}$, $\mathcal{I}\models(P_{1}\sqsubseteq P_{2},m)$. It follows
directly from the definition of the annotated interpretation of
$\mathsf{inv}(P_{1})$ and $\mathsf{inv}(P_{2})$ that
$\mathcal{I}\models(\mathsf{inv}(P_{1})\sqsubseteq\mathsf{inv}(P_{2}),m)$.

  * •

If $(\alpha,{m})$ is of the form
$(\mathsf{inv}(P_{1})\sqcap\mathsf{inv}(P_{2})\sqsubseteq\bot,m)$ for some
$(P_{1}\sqcap P_{2}\sqsubseteq\bot,m)\in\mathcal{O}$, since $\mathcal{I}$ is a
model of $\mathcal{O}$, $(P_{1}\sqcap P_{2})^{\mathcal{I}}=\emptyset$ so
$(\mathsf{inv}(P_{1})\sqcap\mathsf{inv}(P_{2}))^{\mathcal{I}}=\emptyset$.
Hence
$\mathcal{I}\models(\mathsf{inv}(P_{1})\sqcap\mathsf{inv}(P_{2})\sqsubseteq\bot,m)$

Assume that the property is true for all $i\leq N$ and consider
$(\alpha,{m})\in\mathsf{saturate}(\mathcal{O})$ such that $(\alpha,{m})$ has
been added in $\mathsf{saturate}(\mathcal{O})$ at step $N+1$. We have 11
possible cases depending on which completion rule has been applied in step
$N+1$.

$\mathsf{CR}^{T}_{0}$

$(\alpha,{m})=(A\sqsubseteq\bot,{m_{0}\times m_{1}\times m_{2}\times m_{3}})$
and the induction hypothesis applies to $(A\sqsubseteq\exists P,m_{0})$,
$(P\sqsubseteq P_{1},m_{1})$, $(P\sqsubseteq P_{2},m_{2})$ and $(P_{1}\sqcap
P_{2}\sqsubseteq\bot,m_{3})$ so that $\mathcal{I}\models(A\sqsubseteq\exists
P,m_{0})$, $\mathcal{I}\models(P\sqsubseteq P_{1},m_{1})$,
$\mathcal{I}\models(P\sqsubseteq P_{2},m_{2})$ and
$\mathcal{I}\models(P_{1}\sqcap P_{2}\sqsubseteq\bot,m_{3})$. Since
$\bot^{\mathcal{I}}=\emptyset$, then $(P_{1}\sqcap
P_{2})^{\mathcal{I}}=\emptyset$. It follows that $A^{\mathcal{I}}=\emptyset$
(otherwise, if $(c,n)\in A^{\mathcal{I}}$, there would be $(c,d,n\times
m_{0})\in P^{\mathcal{I}}$, so $(c,d,n\times m_{0}\times m_{1})\in
P_{1}^{\mathcal{I}}$ and $(c,d,n\times m_{0}\times m_{2})\in
P_{2}^{\mathcal{I}}$, hence $(c,d,n\times m_{0}\times m_{1}\times
m_{2})\in(P_{1}\sqcap P_{2})^{\mathcal{I}}$). Hence
$\mathcal{I}\models(A\sqsubseteq\bot,m)$ for every $m$, in particular for
$m={m_{0}\times m_{1}\times m_{2}\times m_{3}}$.

$\mathsf{CR}^{T}_{1}$

$(\alpha,{m})=(P_{1}\sqsubseteq P_{3},{m_{1}\times m_{2}})$ and the induction
hypothesis applies to $(P_{1}\sqsubseteq P_{2},m_{1})$ and $(P_{2}\sqsubseteq
P_{3},m_{2})$, so that $\mathcal{I}\models(P_{1}\sqsubseteq P_{2},m_{1})$ and
$\mathcal{I}\models(P_{2}\sqsubseteq P_{3},m_{2})$. If $(c,d,n)\in
P_{1}^{\mathcal{I}}$, then $(c,d,n\times m_{1})\in P_{2}^{\mathcal{I}}$ so
$(c,d,n\times m_{1}\times m_{2})\in P_{3}^{\mathcal{I}}$. Hence
$\mathcal{I}\models(P_{1}\sqsubseteq P_{3},{m_{1}\times m_{2}})$.

$\mathsf{CR}^{T}_{2}$

$(\alpha,{m})=(M\sqcap N\sqsubseteq C,{m_{1}\times m_{2}})$ and the induction
hypothesis applies to $(M\sqsubseteq A,m_{1})$ and $(A\sqcap N\sqsubseteq
C,m_{2})$, so that $\mathcal{I}\models(M\sqsubseteq A,m_{1})$ and
$\mathcal{I}\models(A\sqcap N\sqsubseteq C,m_{2})$. If $(c,n)\in(M\sqcap
N)^{\mathcal{I}}$, there exists $(c,n_{1})\in M^{\mathcal{I}}$ and
$(c,n_{2})\in N^{\mathcal{I}}$ such that $n_{1}\times n_{2}=n$. It follows
that $(c,n_{1}\times m_{1})\in A^{\mathcal{I}}$, so $(c,n_{1}\times
m_{1}\times n_{2})\in(A\sqcap N)^{\mathcal{I}}$ so that $(c,n_{1}\times
m_{1}\times n_{2}\times m_{2})\in C^{\mathcal{I}}$, i.e. $(c,n\times
m_{1}\times m_{2})\in C^{\mathcal{I}}$. Hence $\mathcal{I}\models(M\sqcap
N\sqsubseteq C,{m_{1}\times m_{2}})$.

$\mathsf{CR}^{T}_{3}$

$(\alpha,{m})=(A\sqcap A_{1}\sqcap\dots\sqcap A_{k}\sqsubseteq D,m\times
n\times o\times m_{0}\times\Pi_{i=1}^{k}(m_{i}\times
n_{i})\times\Pi_{i=1}^{k^{\prime}}o_{i})$ and the induction hypothesis applies
to

  * •

$(A\sqsubseteq\exists Q,m_{0})$,

  * •

$(Q\sqsubseteq P,m)$,

  * •

$(Q\sqsubseteq P_{i},m_{i}),(\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq
B_{i},n_{i})$, $1\leq i\leq k$, $k\geq 0$,

  * •

$(\top\sqsubseteq B^{\prime}_{i},o_{i})$, $1\leq i\leq k^{\prime}$,
$k^{\prime}\geq 0$,

  * •

$(B_{1}\sqcap\dots\sqcap B_{k}\sqcap B^{\prime}_{1}\sqcap\dots\sqcap
B^{\prime}_{k^{\prime}}\sqsubseteq C,n),$ and

  * •

$(\exists P.C\sqsubseteq D,o)$.

Let $(c,r)\in(A\sqcap A_{1}\sqcap\dots\sqcap A_{k})^{\mathcal{I}}$. There
exists $(c,r_{0})\in A^{\mathcal{I}}$, and $(c,r_{i})\in A_{i}^{\mathcal{I}}$
for $1\leq i\leq k$ such that $r=r_{0}\times\Pi_{i=1}^{k}r_{i}$.

Since $\mathcal{I}\models(A\sqsubseteq\exists Q,m_{0})$, there exists
$(c,d,r_{0}\times m_{0})\in Q^{\mathcal{I}}$.

For every $1\leq i\leq k$, since $\mathcal{I}\models(Q\sqsubseteq
P_{i},m_{i})$, $(c,d,r_{0}\times m_{0}\times m_{i})\in P_{i}^{\mathcal{I}}$.
Hence, since $(c,r_{i})\in A_{i}^{\mathcal{I}}$, it follows that
$(d,r_{0}\times m_{0}\times m_{i}\times
r_{i})\in(\exists\mathsf{inv}(P_{i}).A_{i})^{\mathcal{I}}$. Since
$\mathcal{I}\models(\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq B_{i},n_{i})$,
then $(d,r_{0}\times m_{0}\times m_{i}\times r_{i}\times n_{i})\in
B_{i}^{\mathcal{I}}$.

For every $1\leq i\leq k^{\prime}$, since $\mathcal{I}\models(\top\sqsubseteq
B^{\prime}_{i},o_{i})$, then $(d,o_{i})\in{B^{\prime}_{i}}^{\mathcal{I}}$.

Since $\times$ is idempotent, it follows that $(d,r_{0}\times
m_{0}\times\Pi_{i=1}^{k}(m_{i}\times r_{i}\times
n_{i})\times\Pi_{i=1}^{k^{\prime}}o_{i})\in(B_{1}\sqcap\dots\sqcap B_{k}\sqcap
B^{\prime}_{1}\sqcap\dots\sqcap B^{\prime}_{k^{\prime}})^{\mathcal{I}}$, i.e.
$(d,r\times m_{0}\times\Pi_{i=1}^{k}(m_{i}\times
n_{i})\times\Pi_{i=1}^{k^{\prime}}o_{i})\in(B_{1}\sqcap\dots\sqcap B_{k}\sqcap
B^{\prime}_{1}\sqcap\dots\sqcap B^{\prime}_{k^{\prime}})^{\mathcal{I}}$.
Hence, since $\mathcal{I}\models(B_{1}\sqcap\dots\sqcap B_{k}\sqcap
B^{\prime}_{1}\sqcap\dots\sqcap B^{\prime}_{k^{\prime}}\sqsubseteq C,n)$,
$(d,r\times m_{0}\times n\times\Pi_{i=1}^{k}(m_{i}\times
n_{i})\times\Pi_{i=1}^{k^{\prime}}o_{i})\in C^{\mathcal{I}}$.

Moreover, since $(Q\sqsubseteq P,m)$, $(c,d,r_{0}\times m_{0}\times m)\in
P^{\mathcal{I}}$, so that $(c,r\times m_{0}\times m\times
n\times\Pi_{i=1}^{k}(m_{i}\times
n_{i})\times\Pi_{i=1}^{k^{\prime}}o_{i})\in(\exists P.C)^{\mathcal{I}}$ since
$\times$ is idempotent.

Finally, $\mathcal{I}\models(\exists P.C\sqsubseteq D,o)$ so $(c,r\times
m_{0}\times m\times n\times o\times\Pi_{i=1}^{k}(m_{i}\times
n_{i})\times\Pi_{i=1}^{k^{\prime}}o_{i})\in D^{\mathcal{I}}$. Hence
$\mathcal{I}\models(A\sqcap A_{1}\sqcap\dots\sqcap A_{k}\sqsubseteq D,m\times
n\times o\times m_{0}\times\Pi_{i=1}^{k}(m_{i}\times
n_{i})\times\Pi_{i=1}^{k^{\prime}}o_{i})$.

$\mathsf{CR}^{A}_{1}$

$(\alpha,{m})=(B(a),{m_{1}\times\dots\times m_{k}\times m})$ and the induction
hypothesis applies to $(A_{i}(a),m_{i})$, $1\leq i\leq k$, and
$(A_{1}\sqcap\dots\sqcap A_{k}\sqsubseteq B,m)$, so that
$\mathcal{I}\models(A_{i}(a),m_{i})$, $1\leq i\leq k$, and
$\mathcal{I}\models(A_{1}\sqcap\dots\sqcap A_{k}\sqsubseteq B,m)$. It follows
that $(a^{\mathcal{I}},m_{1}\times\dots\times m_{k})\in(A_{1}\sqcap\dots\sqcap
A_{n})^{\mathcal{I}}$, so $(a^{\mathcal{I}},m_{1}\times\dots\times m_{k}\times
m)\in B^{\mathcal{I}}$. Hence $\mathcal{I}\models(B(a),{m_{1}\times\dots\times
m_{k}\times m})$.

$\mathsf{CR}^{A}_{2}$

to $\mathsf{CR}^{A}_{5}$ are easy to show in a similar way.

$\mathsf{CR}^{A}_{6}$

and $\mathsf{CR}^{A}_{7}$ are never applied because $\mathcal{O}$ is
consistent. We show this for $\mathsf{CR}^{A}_{6}$ case. Assume for a
contradiction that $(\alpha,{m})=(\bot(a),{m_{1}\times m_{2}\times m_{3}})$
has been added to $\mathsf{saturate}(\mathcal{O})$ by $\mathsf{CR}^{A}_{6}$.
In this case, the induction hypothesis applies to $(R(a,b),m_{1})$,
$(S(a,b),m_{2})$ and $(R\sqcap S\sqsubseteq\bot,m_{3})$, so that
$\mathcal{I}\models(R(a,b),m_{1})$, $\mathcal{I}\models(S(a,b),m_{2})$ and
$\mathcal{I}\models(R\sqcap S\sqsubseteq\bot,m_{3})$. It must be the case that
$(R\sqcap S)^{\mathcal{I}}=\emptyset$ while
$(a^{\mathcal{I}},b^{\mathcal{I}},m_{1}\times m_{2})\in(R\sqcap
S)^{\mathcal{I}}$, which is a contradiction. Hence $\mathsf{CR}^{A}_{6}$ is
never applied when $\mathcal{O}$ is consistent.

This concludes the proof of the lemma. ∎

The following lemma wil be useful to handle RIs in the proofs of this section.

######  Lemma B.9.

If $(P_{1}\sqsubseteq P_{2},m)\in\mathsf{saturate}(\mathcal{O})$, then
$(\mathsf{inv}(P_{1})\sqsubseteq\mathsf{inv}(P_{2}),m)\in\mathsf{saturate}(\mathcal{O})$.

###### Proof.

We show by induction on the number of completion rules applied before adding
$(P_{1}\sqsubseteq P_{2},m)$ to $\mathsf{saturate}(\mathcal{O})$ that
$(\mathsf{inv}(P_{1})\sqsubseteq\mathsf{inv}(P_{2}),m)\in\mathsf{saturate}(\mathcal{O})$.

  * •

Base case: $(P_{1}\sqsubseteq P_{2},m)\in\mathcal{S}$. If $(P_{1}\sqsubseteq
P_{2},m)\in\mathcal{O}$ then
$(\mathsf{inv}(P_{1})\sqsubseteq\mathsf{inv}(P_{2}),m)\in\mathcal{S}$.
Otherwise, $(P_{1}\sqsubseteq P_{2},m)\in\mathcal{S}\setminus\mathcal{O}$ and
there is two possibilities by definition of $\mathcal{S}$: either
$(P_{1}\sqsubseteq P_{2},m)=(P\sqsubseteq P,1)$, or $(P_{1}\sqsubseteq
P_{2},m)=(\mathsf{inv}(P_{3})\sqsubseteq\mathsf{inv}(P_{4}),m)$ for some
$(P_{3}\sqsubseteq P_{4},m)\in\mathcal{O}$. Since for every $R$, both
$(R\sqsubseteq R,1)$ and $(R^{-}\sqsubseteq R^{-},1)$ are in $\mathcal{S}$ and
$\mathsf{inv}(\mathsf{inv}(P))=P$, it follows that in every case,
$(\mathsf{inv}(P_{1})\sqsubseteq\mathsf{inv}(P_{2}),m)\in\mathsf{saturate}(\mathcal{O})$.

  * •

Assume that for every $(P\sqsubseteq Q,m)\in\mathsf{saturate}(\mathcal{O})$
obtained after at most $k$ applications of the completion rules,
$(\mathsf{inv}(P)\sqsubseteq\mathsf{inv}(Q),m)\in\mathsf{saturate}(\mathcal{O})$,
and let $(P_{1}\sqsubseteq P_{2},m)\in\mathsf{saturate}(\mathcal{O})$ be
obtained after applying $k+1$ completion rules. Since the only completion rule
that adds role inclusions is $\mathsf{CR}^{T}_{1}$, $(P_{1}\sqsubseteq
P_{2},m)$ has been added by applying $\mathsf{CR}^{T}_{1}$ to some
$(P_{1}\sqsubseteq P^{\prime},m_{1})$ and $(P^{\prime}\sqsubseteq
P_{2},m_{2})$ in $\mathsf{saturate}(\mathcal{O})$ such that $m_{1}\times
m_{2}=m$. By induction hypothesis,
$(\mathsf{inv}(P_{1})\sqsubseteq\mathsf{inv}(P^{\prime}),m_{1})$ and
$(\mathsf{inv}(P^{\prime})\sqsubseteq\mathsf{inv}(P_{2}),m_{2})$ are in
$\mathsf{saturate}(\mathcal{O})$. Hence, by $\mathsf{CR}^{T}_{1}$,
$(\mathsf{inv}(P_{1})\sqsubseteq\mathsf{inv}(P_{2}),m)\in\mathsf{saturate}(\mathcal{O})$.
∎

For point (2) of Theorem 4.7, i.e. completeness of the completion algorithm,
we will use the canonical model $\mathcal{I}_{\mathcal{O}}=\bigcup_{i\geq
0}\mathcal{I}_{i}$ of $\mathcal{O}$ (cf. Figure 2). The next lemmas will be
crucial to handle the anonymous part of the canonical model in several proofs.

######  Lemma B.10.

For all $i\geq 0$, $x,y\in\Delta^{\mathcal{I}_{\mathcal{O}}}$ and $R$ role
name or inverse role, if $(x,y,o)\in R^{\mathcal{I}_{i}}$ and $y\notin{\sf
N_{I}}$ has been introduced between $\mathcal{I}_{j-1}$ and $\mathcal{I}_{j}$
($j\leq i$) to satisfy an inclusion of the form $(C\sqsubseteq\exists
S,m_{0})\in\mathcal{O}$ by applying $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ to
some $(x,s)\in C^{\mathcal{I}_{j-1}}$, then there exists $(S\sqsubseteq
R,m_{S\sqsubseteq R})\in\mathsf{saturate}(\mathcal{O})$ such that $s\times
m_{0}\times m_{S\sqsubseteq R}=o$.

###### Proof.

The proof is by induction on $l=i-j$.

_Base case: $l=0$._ The only possibility to obtain $(x,y,o)\in
R^{\mathcal{I}_{i}}$ by applying a single rule that introduces $y$ to satisfy
an inclusion of the form $(C\sqsubseteq\exists S,m_{0})$ with some $(x,s)\in
C^{\mathcal{I}_{i-1}}$ is that $S=R$ and $s\times m_{0}=o$. Since
$(R\sqsubseteq R,1)\in\mathsf{saturate}(\mathcal{O})$, we obtain the property.

_Inductive step._ Assume that the property is true for every integer up to $l$
and consider the case where $i-j=l+1$. Let
$x,y\in\Delta^{\mathcal{I}_{\mathcal{O}}}$, and assume that $(x,y,o)\in
R^{\mathcal{I}_{i}}$, and $y\notin{\sf N_{I}}$ has been introduced between
$\mathcal{I}_{j-1}$ and $\mathcal{I}_{j}$, to satisfy $(C\sqsubseteq\exists
S,m_{0})\in\mathcal{O}$ by applying $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ to
$(x,s)\in C^{\mathcal{I}_{j-1}}$ (thus adding $(x,y,s\times m_{0})\in
S^{\mathcal{I}_{j}}$). We make a case analysis on whether $(x,y,o)\in
R^{\mathcal{I}_{i}}$ has been added by applying $\mathsf{R}_{1}$ or
$\mathsf{R}_{2}$ with a RI of the form:

  * •

$(P_{p-1}\sqsubseteq R,r_{p})\in\mathcal{O}$: It holds that
$(x,y,o^{\prime\prime})\in P_{p-1}^{\mathcal{I}_{i-1}}$ (with
$o=o^{\prime\prime}\times r_{p}$) so by induction hypothesis (since $i-1-j=l$
and the property is assumed to be true for $l$), there exists $(S\sqsubseteq
P_{p-1},m_{S\sqsubseteq P_{p-1}})\in\mathsf{saturate}(\mathcal{O})$ such that
$s\times m_{0}\times m_{S\sqsubseteq P_{p-1}}=o^{\prime\prime}$, which implies
by $\mathsf{CR}^{T}_{1}$ that $(S\sqsubseteq R,m_{S\sqsubseteq
R})\in\mathsf{saturate}(\mathcal{O})$ with $m_{S\sqsubseteq R}=m_{S\sqsubseteq
P_{p-1}}\times r_{p}$ so that $s\times m_{0}\times m_{S\sqsubseteq
R}=o^{\prime\prime}\times r_{p}=o$.

  * •

$(P_{p-1}\sqsubseteq\mathsf{inv}(R),r_{p})\in\mathcal{O}$: It holds that
$(x,y,o^{\prime\prime})\in\mathsf{inv}(P_{p-1})^{\mathcal{I}_{i-1}}$ (with
$o=o^{\prime\prime}\times r_{p}$) so by induction hypothesis there exists
$(S\sqsubseteq\mathsf{inv}(P_{p-1}),m_{S\sqsubseteq\mathsf{inv}(P_{p-1})})\in\mathsf{saturate}(\mathcal{O})$
with $s\times m_{0}\times
m_{S\sqsubseteq\mathsf{inv}(P_{p-1})}=o^{\prime\prime}$. Since
$(P_{p-1}\sqsubseteq\mathsf{inv}(R),r_{p})\in\mathsf{saturate}(\mathcal{O})$,
by Lemma B.9, $(\mathsf{inv}(P_{p-1})\sqsubseteq
R,r_{p})\in\mathsf{saturate}(\mathcal{O})$. Hence, by $\mathsf{CR}^{T}_{1}$
$(S\sqsubseteq R,m_{S\sqsubseteq R})\in\mathsf{saturate}(\mathcal{O})$ with
$m_{S\sqsubseteq R}=m_{S\sqsubseteq\mathsf{inv}(P_{p-1})}\times r_{p}$ so that
$s\times m_{0}\times m_{S\sqsubseteq R}=o^{\prime\prime}\times r_{p}=o$. ∎

######  Lemma B.11.

For all $i\geq 0$, $x,y\in\Delta^{\mathcal{I}_{\mathcal{O}}}$ and $A\in{\sf
N_{C}}\cup\\{\top\\}$ if $(y,o^{\prime})\in A^{\mathcal{I}_{i}}$ and
$y\notin{\sf N_{I}}$ has been introduced between $\mathcal{I}_{j-1}$ and
$\mathcal{I}_{j}$ ($j\leq i$) to satisfy an inclusion of the form
$(C\sqsubseteq\exists S,m_{0})\in\mathcal{O}$ by applying $\mathsf{R}_{6}$ or
$\mathsf{R}_{7}$ to some $(x,s)\in C^{\mathcal{I}_{j-1}}$, then the following
holds.

  1. 1.

There exist $k\geq 0$ and $k^{\prime}\geq 0$ such that:

     * •

$(S\sqsubseteq P_{i},m_{S\sqsubseteq P_{i}})$ and
$(\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq
B_{i},m_{\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq
B_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k$,

     * •

$(\top\sqsubseteq B^{\prime}_{i},m_{\top\sqsubseteq
B^{\prime}_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k^{\prime}$,

     * •

$(B_{1}\sqcap\dots\sqcap B_{k}\sqcap B^{\prime}_{1}\sqcap\dots\sqcap
B^{\prime}_{k^{\prime}}\sqsubseteq A,p)\in\mathsf{saturate}(\mathcal{O})$.

Moreover, if $A=\top$, then $k=k^{\prime}=0$ and $p=1$ (recall that the empty
conjunction is $\top$ and
$(\top\sqsubseteq\top,1)\in\mathsf{saturate}(\mathcal{O})$).

  2. 2.

For every $1\leq\ell\leq k$, there exists $(x,s_{\ell})\in
A_{\ell}^{\mathcal{I}_{i-1}}$.

  3. 3.

The monomials are related as follows:

     * •

If $k\neq 0$, $s\times
m_{0}\times\Pi_{\ell=1}^{k}s_{\ell}\times\Pi_{i=1}^{k}(m_{S\sqsubseteq
P_{i}}\times m_{\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p=o^{\prime}$.

     * •

If $k=0$, $\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p=o^{\prime}$.

###### Proof.

The proof is by induction on $l=i-j$. In the case where $A=\top$, the property
trivially holds with $k=k^{\prime}=0$ for every $l\geq 0$.

_Base case._ In the case where $A\neq\top$, the base case is $l=1$:
$y\notin{\sf N_{I}}$ has been introduced between $\mathcal{I}_{i-2}$ and
$\mathcal{I}_{i-1}$ to satisfy $(C\sqsubseteq\exists S,m_{0})$ by applying
$\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ to $(x,s)\in C^{\mathcal{I}_{i-2}}$,
adding $(x,y,o)\in S^{\mathcal{I}_{i-1}}$. By construction of
$\mathcal{I}_{\mathcal{O}}$, it must be the case that either (i) the rule
corresponding to $(\exists\mathsf{inv}(S).\top\sqsubseteq A,m_{1})$
($\mathsf{R}_{5}$ or $\mathsf{R}_{4}$) has been applied between
$\mathcal{I}_{i-1}$ and $\mathcal{I}_{i}$, so that
$(\exists\mathsf{inv}(S).\top\sqsubseteq A,m_{1})\in\mathcal{O}$, and $s\times
m_{0}\times m_{1}=o^{\prime}$, or (ii) the rule corresponding to
$(\top\sqsubseteq A,m_{1})$ ($\mathsf{R}_{3}$) has been applied between
$\mathcal{I}_{i-1}$ and $\mathcal{I}_{i}$, so that $(\top\sqsubseteq
A,m_{1})\in\mathcal{O}$, and $m_{1}=o^{\prime}$. This shows the property in
this case:

  1. 1.

In case (i), for $k=1$ and $k^{\prime}=0$ it holds that

     * •

$(S\sqsubseteq S,1)$ and $(\exists\mathsf{inv}(S).\top\sqsubseteq
A,m_{1})\in\mathsf{saturate}(\mathcal{O})$ (take $P_{1}=S$, $A_{1}=\top$,
$B_{1}=A$ and $m_{S\sqsubseteq P_{1}}=1$,
$m_{\mathsf{inv}(P_{1}).A_{1}\sqsubseteq B_{1}}=m_{1}$),

     * •

$(A\sqsubseteq A,1)\in\mathsf{saturate}(\mathcal{O})$ (take $B_{1}=A$ and
$p=1$).

In case (ii), for $k=0$ and $k^{\prime}=1$, it holds that

     * •

$(\top\sqsubseteq A,m_{1})\in\mathsf{saturate}(\mathcal{O})$ (take
$B^{\prime}_{1}=A$ and $m_{\top\sqsubseteq B^{\prime}_{i}}=m_{1}$)

     * •

$(A\sqsubseteq A,1)\in\mathsf{saturate}(\mathcal{O})$ (take $B^{\prime}_{1}=A$
and $p=1$).

  2. 2.

In the case $k=1$, $(x,1)\in\top^{\mathcal{I}_{i-1}}$ holds trivially (take
$A_{1}=\top$ and $s_{1}=1$).

  3. 3.

The monomials are related as follows:

     * •

If $k\neq 0$, we are in case (i) and $s\times m_{0}\times 1\times 1\times
m_{1}\times 1=o^{\prime}$.

     * •

If $k=0$, we are in case (ii) and $m_{1}\times 1=o^{\prime}$.

_Inductive step._ Assume that the property is true for every integer up to $l$
and consider the case where $i-j=l+1$. Let
$x,y\in\Delta^{\mathcal{I}_{\mathcal{O}}}$, and assume that $(y,o^{\prime})\in
A^{\mathcal{I}_{i}}$, and $y\notin{\sf N_{I}}$ has been introduced between
$\mathcal{I}_{j-1}$ and $\mathcal{I}_{j}$, to satisfy $(C\sqsubseteq\exists
S,m_{0})\in\mathcal{O}$ by applying $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ to
$(x,s)\in C^{\mathcal{I}_{j-1}}$ (thus adding $(x,y,s\times m_{0})\in
S^{\mathcal{I}_{j}}$). We make a case analysis on the last rule applied to add
$(y,o^{\prime})\in A^{\mathcal{I}_{i}}$ (among $\mathsf{R}_{3}$,
$\mathsf{R}_{4}$ and $\mathsf{R}_{5}$).

$\bullet$ Case $\boldsymbol{(y,o^{\prime})\in A^{\mathcal{I}_{i}}}$ added by
applying $\boldsymbol{\mathsf{R}_{3}}$ with $\boldsymbol{(D_{1}\sqcap
D_{2}\sqsubseteq A,m_{D_{1}\sqcap D_{2}\sqsubseteq A})\in\mathcal{O}}$. There
are $(y,o_{1})\in D_{1}^{\mathcal{I}_{i-1}}$ and $(y,o_{2})\in
D_{2}^{\mathcal{I}_{i-1}}$ and $o^{\prime}=m_{D_{1}\sqcap D_{2}\sqsubseteq
A}\times o_{1}\times o_{2}$. For $j\in\\{1,2\\}$, since $(y,o_{j})\in
D_{j}^{\mathcal{I}_{i-1}}$, by induction hypothesis:

  1. 1.

There exist $k_{j}\geq 0$ and $k_{j}^{\prime}\geq 0$ such that:

     * •

$(S\sqsubseteq P^{j}_{i},m_{S\sqsubseteq P^{j}_{i}})$,
$(\exists\mathsf{inv}(P_{i}^{j}).A^{j}_{i}\sqsubseteq
B^{j}_{i},m_{\exists\mathsf{inv}(P_{i}^{j}).A^{j}_{i}\sqsubseteq
B^{j}_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k_{j}$,

     * •

$(\top\sqsubseteq B^{\prime j}_{i},m_{\top\sqsubseteq B^{\prime
j}_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k_{j}^{\prime}$,

     * •

$(B^{j}_{1}\sqcap\dots\sqcap B^{j}_{k_{j}}\sqcap B^{\prime
j}_{1}\sqcap\dots\sqcap B^{\prime j}_{k_{j}^{\prime}}\sqsubseteq
D_{j},p_{j})\in\mathsf{saturate}(\mathcal{O})$.

  2. 2.

For every $1\leq\ell\leq k_{j}$, there exists
$(x,s^{j}_{\ell})\in{A^{j}_{\ell}}^{\mathcal{I}_{i-2}}$.

  3. 3.

The monomials are related as follows:

     * •

If $k_{j}\neq 0$, $s\times
m_{0}\times\Pi_{\ell=1}^{k_{j}}s^{j}_{\ell}\times\Pi_{i=1}^{k_{j}}(m_{S\sqsubseteq
P^{j}_{i}}\times m_{\exists\mathsf{inv}(P_{i}^{j}).A^{j}_{i}\sqsubseteq
B^{j}_{i}})\times\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq B^{\prime
j}_{i}}\times p_{j}=o_{j}$.

     * •

If $k_{j}=0$, $\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq B^{\prime
j}_{i}}\times p_{j}=o_{j}$.

Since $(D_{1}\sqcap D_{2}\sqsubseteq A,m_{D_{1}\sqcap D_{2}\sqsubseteq
A})\in\mathsf{saturate}(\mathcal{O})$ and $(B^{1}_{1}\sqcap\dots\sqcap
B^{1}_{k_{1}}\sqcap B^{\prime 1}_{1}\sqcap\dots\sqcap B^{\prime
1}_{k_{1}^{\prime}}\sqsubseteq D_{1},p_{1})\in\mathsf{saturate}(\mathcal{O})$,
by $\mathsf{CR}^{T}_{2}$, $(B^{1}_{1}\sqcap\dots\sqcap B^{1}_{k_{1}}\sqcap
B^{\prime 1}_{1}\sqcap\dots\sqcap B^{\prime 1}_{k_{1}^{\prime}}\sqcap
D_{2}\sqsubseteq A,m_{D_{1}\sqcap D_{2}\sqsubseteq A}\times
p_{1})\in\mathsf{saturate}(\mathcal{O})$. By applying again
$\mathsf{CR}^{T}_{2}$, we obtain
$(\bigsqcap_{j=1}^{2}(B^{j}_{1}\sqcap\dots\sqcap B^{j}_{k_{j}}\sqcap B^{\prime
j}_{1}\sqcap\dots\sqcap B^{\prime j}_{k_{j}^{\prime}})\sqsubseteq
A,p)\in\mathsf{saturate}(\mathcal{O})$ with $p=m_{D_{1}\sqcap D_{2}\sqsubseteq
A}\times p_{1}\times p_{2}$.

If we let $k=k_{1}+k_{2}$, $k^{\prime}=k^{\prime}_{1}+k^{\prime}_{2}$,
$f(i,j)=\Sigma_{\ell=1}^{j-1}k_{\ell}+i$ and
$f^{\prime}(i,j)=\Sigma_{\ell=1}^{j-1}k^{\prime}_{\ell}+i$, we can rename the
$P_{i}^{j}$, $A_{i}^{j}$, $B_{i}^{j}$, ${B^{\prime}_{i}}^{j}$ and
$s_{\ell}^{j}$ by $P_{f(i,j)}$, $A_{f(i,j)}$, $B_{f(i,j)}$,
$B^{\prime}_{f^{\prime}(i,j)}$ and $s_{f(\ell,j)}$ respectively to obtain
items 1 and 2 of the property. To obtain item 3 of the property, we observe
that the monomials are related as follows:

If $k\neq 0$, i.e. $k_{1}\neq 0$ or $k_{2}\neq 0$:

$\displaystyle o^{\prime}=$ $\displaystyle m_{D_{1}\sqcap D_{2}\sqsubseteq
A}\times o_{1}\times o_{2}$ $\displaystyle=$ $\displaystyle m_{D_{1}\sqcap
D_{2}\sqsubseteq A}\times s\times
m_{0}\times\Pi_{j=1}^{2}(\Pi_{\ell=1}^{k_{j}}s^{j}_{\ell}\times\Pi_{i=1}^{k_{j}}(m_{S\sqsubseteq
P^{j}_{i}}\times m_{\exists\mathsf{inv}(P_{i}^{j}).A^{j}_{i}\sqsubseteq
B^{j}_{i}})\times\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq B^{\prime
j}_{i}}\times p_{j})$ $\displaystyle=$ $\displaystyle s\times m_{0}\times
m_{D_{1}\sqcap D_{2}\sqsubseteq A}\times\Pi_{j=1}^{2}p_{j}$
$\displaystyle\times\Pi_{j=1}^{2}\Pi_{\ell=1}^{k_{j}}s^{j}_{\ell}\times\Pi_{j=1}^{2}\Pi_{i=1}^{k_{j}}(m_{S\sqsubseteq
P^{j}_{i}}\times m_{\exists\mathsf{inv}(P_{i}^{j}).A^{j}_{i}\sqsubseteq
B^{j}_{i}})\times\Pi_{j=1}^{2}\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq
B^{\prime j}_{i}}$ $\displaystyle=$ $\displaystyle s\times m_{0}\times
p\times\Pi_{\ell=1}^{k}s_{\ell}\times\Pi_{i=1}^{k}(m_{S\sqsubseteq
P_{i}}\times m_{\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}.$

If $k=0$, i.e. $k_{1}=k_{2}=0$:

$\displaystyle o^{\prime}=m_{D_{1}\sqcap D_{2}\sqsubseteq A}\times o_{1}\times
o_{2}=m_{D_{1}\sqcap D_{2}\sqsubseteq
A}\times\Pi_{j=1}^{2}(\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq B^{\prime
j}_{i}}\times p_{j})=p\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq
B^{\prime}_{i}}.$

This shows the property in this case.

$\bullet$ Case $\boldsymbol{(y,o^{\prime})\in A^{\mathcal{I}_{i}}}$ added by
applying $\boldsymbol{\mathsf{R}_{4}}$ or $\boldsymbol{\mathsf{R}_{5}}$ with
$\boldsymbol{(\exists P.D\sqsubseteq A,m_{\exists P.D\sqsubseteq
A})\in\mathcal{O}}$. There exist $(y,z,o_{yz})\in P^{\mathcal{I}_{i-1}}$ and
$(z,o_{z})\in D^{\mathcal{I}_{i-1}}$ such that $o^{\prime}=o_{yz}\times
o_{z}\times m_{\exists P.D\sqsubseteq A}$. We distinguish two subcases:

  1. (i)

either $z=x$,

  2. (ii)

or $z\neq x$, which implies that $z$ has been introduced between
$j^{\prime}-1$ and $j^{\prime}$ ($j\leq j^{\prime}\leq i$) to satisfy an
inclusion of the form $(E_{0}\sqsubseteq\exists S_{z},m_{z})\in\mathcal{O}$ by
applying $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$.

We start with case (i). It holds that $(y,x,o_{yx})\in P^{\mathcal{I}_{i-1}}$,
$(x,o_{x})\in D^{\mathcal{I}_{i-1}}$ and $o^{\prime}=o_{yx}\times o_{x}\times
m_{\exists P.D\sqsubseteq A}$. Since $(y,x,o_{yx})\in P^{\mathcal{I}_{i-1}}$,
i.e. $(x,y,o_{yx})\in\mathsf{inv}(P)^{\mathcal{I}_{i-1}}$, and $y$ has been
introduced to satisfy $(C\sqsubseteq\exists S,m_{0})\in\mathcal{O}$ by
applying $\mathsf{R}_{6}$ to some $(x,s)\in C^{\mathcal{I}_{j-1}}$, then by
Lemma B.10, there is
$(S\sqsubseteq\mathsf{inv}(P),m_{S\sqsubseteq\mathsf{inv}(P)})\in\mathsf{saturate}(\mathcal{O})$
such that $s\times m_{0}\times m_{S\sqsubseteq\mathsf{inv}(P)}=o_{yx}$. This
shows the property in case (i), indeed:

  1. 1.

If we take $k=1$ and $k^{\prime}=0$, it holds that:

     * •

$(S\sqsubseteq\mathsf{inv}(P),m_{S\sqsubseteq\mathsf{inv}(P)})$ and $(\exists
P.D\sqsubseteq A,m_{\exists P.D\sqsubseteq
A})\in\mathsf{saturate}(\mathcal{O})$ (take $P_{1}=\mathsf{inv}(P)$,
$A_{1}=D$, $B_{1}=A$),

     * •

$(A\sqsubseteq A,1)\in\mathsf{saturate}(\mathcal{O})$ (take $B_{1}=A$ and
$p=1$).

  2. 2.

$(x,o_{x})\in D^{\mathcal{I}_{i-1}}$ (take $A_{1}=D$ and $s_{1}=o_{x}$).

  3. 3.

The monomials are related as follows (and $k\neq 0$):

$\displaystyle o^{\prime}=o_{yx}\times o_{x}\times m_{\exists P.D\sqsubseteq
A}=s\times m_{0}\times o_{x}\times m_{S\sqsubseteq\mathsf{inv}(P)}\times
m_{\exists P.D\sqsubseteq A}\times 1.$

We now consider case (ii): $(y,z,o_{yz})\in P^{\mathcal{I}_{i-1}}$,
$(z,o_{z})\in D^{\mathcal{I}_{i-1}}$, $o^{\prime}=o_{yz}\times o_{z}\times
m_{\exists P.D\sqsubseteq A}$ and $z$ has been introduced between
$j^{\prime}-1$ and $j^{\prime}$ ($j\leq j^{\prime}\leq i$) to satisfy an
inclusion of the form $(E_{0}\sqsubseteq\exists S_{z},m_{z})\in\mathcal{O}$ by
applying $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$. There must exist a monomial
$s_{0}$ such that $(y,s_{0})\in E_{0}^{\mathcal{I}_{j^{\prime}-1}}$ to which
$\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ has been applied to satisfy
$(E_{0}\sqsubseteq\exists S_{z},m_{z})$. Hence by Lemma B.10 there exists
$(S_{z}\sqsubseteq P,m_{S_{z}\sqsubseteq P})\in\mathsf{saturate}(\mathcal{O})$
such that $s_{0}\times m_{z}\times m_{S_{z}\sqsubseteq P}=o_{yz}$, and by
induction hypothesis, the following statements hold.

  * •

There exist $k\geq 0$ and $k^{\prime}\geq 0$ such that:

    * –

$(S_{z}\sqsubseteq P_{i},m_{S_{z}\sqsubseteq P_{i}})$ and
$(\exists\mathsf{inv}(P_{i}).E_{i}\sqsubseteq
B_{i},m_{\exists\mathsf{inv}(P_{i}).E_{i}\sqsubseteq
B_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k$,

    * –

$(\top\sqsubseteq B^{\prime}_{i},m_{\top\sqsubseteq
B^{\prime}_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k^{\prime}$,

    * –

$(B_{1}\sqcap\dots\sqcap B_{k}\sqcap B^{\prime}_{1}\sqcap\dots\sqcap
B^{\prime}_{k^{\prime}}\sqsubseteq D,p_{z})\in\mathsf{saturate}(\mathcal{O})$.

Since $(\exists P.D\sqsubseteq A,m_{\exists P.D\sqsubseteq A})\in\mathcal{O}$
and $(E_{0}\sqsubseteq\exists S_{z},m_{z})\in\mathcal{O}$, it follows by
$\mathsf{CR}^{T}_{3}$ that $(E_{0}\sqcap E_{1}\sqcap\dots\sqcap
E_{k}\sqsubseteq A,r_{z})\in\mathsf{saturate}(\mathcal{O})$ with
$r_{z}=m_{z}\times m_{\exists P.D\sqsubseteq A}\times m_{S_{z}\sqsubseteq
P}\times\Pi_{i=1}^{k}(m_{S_{z}\sqsubseteq P_{i}}\times
m_{\exists\mathsf{inv}(P_{i}).E_{i}\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p_{z}$.

  * •

For every $1\leq\ell\leq k$, there exists $(y,s_{\ell})\in
E_{\ell}^{\mathcal{I}_{i-1}}$.

  * •

The monomials are related as follows:

    * –

If $k\neq 0$, $s_{0}\times
m_{z}\times\Pi_{\ell=1}^{k}s_{\ell}\times\Pi_{i=1}^{k}(m_{S_{z}\sqsubseteq
P_{i}}\times m_{\exists\mathsf{inv}(P_{i}).E_{i}\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p_{z}=o_{z}$.

    * –

If $k=0$, $\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p_{z}=o_{z}$.

For every $0\leq j\leq k$, since $(y,s_{j})\in E_{j}^{\mathcal{I}_{i-1}}$, by
induction hypothesis:

  * •

There exist $k_{j}\geq 0$ and $k_{j}^{\prime}\geq 0$ such that:

    * –

$(S\sqsubseteq P^{j}_{i},m_{S\sqsubseteq P^{j}_{i}})$,
$(\exists\mathsf{inv}(P_{i}^{j}).A^{j}_{i}\sqsubseteq
B^{j}_{i},m_{\exists\mathsf{inv}(P_{i}^{j}).A^{j}_{i}\sqsubseteq
B^{j}_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k_{j}$,

    * –

$(\top\sqsubseteq B^{\prime j}_{i},m_{\top\sqsubseteq B^{\prime
j}_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k_{j}^{\prime}$,

    * –

$(B^{j}_{1}\sqcap\dots\sqcap B^{j}_{k_{j}}\sqcap B^{\prime
j}_{1}\sqcap\dots\sqcap B^{\prime j}_{k_{j}^{\prime}}\sqsubseteq
E_{j},p_{j})\in\mathsf{saturate}(\mathcal{O})$.

  * •

For every $1\leq\ell\leq k_{j}$, there exists
$(x,s^{j}_{\ell})\in{A^{j}_{\ell}}^{\mathcal{I}_{i-1}}$.

  * •

The monomials are related as follows:

    * –

If $k_{j}\neq 0$, $s\times
m_{0}\times\Pi_{\ell=1}^{k_{j}}s^{j}_{\ell}\times\Pi_{i=1}^{k_{j}}(m_{S\sqsubseteq
P^{j}_{i}}\times m_{\exists\mathsf{inv}(P_{i}^{j}).A^{j}_{i}\sqsubseteq
B^{j}_{i}})\times\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq{B^{\prime}}^{j}_{i}}\times
p_{j}=s_{j}$.

    * –

If $k_{j}=0$,
$\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq{B^{\prime}}^{j}_{i}}\times
p_{j}=s_{j}$.

Since $(E_{0}\sqcap E_{1}\sqcap\dots\sqcap E_{k}\sqsubseteq
A,r_{z})\in\mathsf{saturate}(\mathcal{O})$ and $(B^{0}_{1}\sqcap\dots\sqcap
B^{0}_{k_{0}}\sqcap B^{\prime 0}_{1}\sqcap\dots\sqcap B^{\prime
0}_{k_{0}^{\prime}}\sqsubseteq E_{1},p_{1})\in\mathsf{saturate}(\mathcal{O})$,
by $\mathsf{CR}^{T}_{2}$, $(B^{0}_{1}\sqcap\dots\sqcap B^{0}_{k_{0}}\sqcap
B^{\prime 0}_{1}\sqcap\dots\sqcap B^{\prime 0}_{k_{0}^{\prime}}\sqcap
E_{1}\sqcap\dots\sqcap E_{k}\sqsubseteq A,r_{z}\times
p_{1})\in\mathsf{saturate}(\mathcal{O})$. By applying successively
$\mathsf{CR}^{T}_{2}$, we obtain
$(\bigsqcap_{j=0}^{k}(B^{j}_{1}\sqcap\dots\sqcap B^{j}_{k_{j}}\sqcap B^{\prime
j}_{1}\sqcap\dots\sqcap B^{\prime j}_{k_{j}^{\prime}})\sqsubseteq
A,p)\in\mathsf{saturate}(\mathcal{O})$ with $p=r_{z}\times\Pi_{j=0}^{k}p_{j}$.

If we let $K=\Sigma_{j=0}^{k}k_{j}$,
$K^{\prime}=\Sigma_{j=1}^{k}k^{\prime}_{j}$, and rename the $P_{i}^{j}$,
$A_{i}^{j}$, $B_{i}^{j}$, ${B^{\prime}_{i}}^{j}$ and $s^{j}_{\ell}$, we obtain
items 1 and 2 of the property. We now show item 3 of the property. Recall that
$r_{z}=m_{z}\times m_{\exists P.D\sqsubseteq A}\times m_{S_{z}\sqsubseteq
P}\times\Pi_{i=1}^{k}(m_{S_{z}\sqsubseteq P_{i}}\times
m_{\exists\mathsf{inv}(P_{i}).E_{i}\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p_{z}$.

If $k\neq 0$, it holds that

$\displaystyle o^{\prime}=$ $\displaystyle o_{yz}\times o_{z}\times m_{\exists
P.D\sqsubseteq A}$ $\displaystyle=$ $\displaystyle s_{0}\times m_{z}\times
m_{S_{z}\sqsubseteq
P}\times\Pi_{j=1}^{k}s_{j}\times\Pi_{i=1}^{k}(m_{S_{z}\sqsubseteq P_{i}}\times
m_{\exists\mathsf{inv}(P_{i}).E_{i}\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p_{z}\times m_{\exists P.D\sqsubseteq A}$ $\displaystyle=$
$\displaystyle\Pi_{j=0}^{k}s_{j}\times\Pi_{i=1}^{k}(m_{S_{z}\sqsubseteq
P_{i}}\times m_{\exists\mathsf{inv}(P_{i}).E_{i}\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p_{z}\times m_{z}\times m_{S_{z}\sqsubseteq P}\times m_{\exists P.D\sqsubseteq
A}$ $\displaystyle=$ $\displaystyle\Pi_{j=0}^{k}s_{j}\times r_{z}.$

If $k=0$, it holds that

$\displaystyle o^{\prime}=o_{yz}\times o_{z}\times m_{\exists P.D\sqsubseteq
A}=s_{0}\times m_{z}\times m_{S_{z}\sqsubseteq
P}\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p_{z}\times m_{\exists P.D\sqsubseteq A}=s_{0}\times r_{z}.$

In both cases, $o^{\prime}=\Pi_{j=0}^{k}s_{j}\times r_{z}$. Recall that
$p=r_{z}\times\Pi_{j=0}^{k}p_{j}$.

In the case where $K\neq 0$, there is some $k_{j}\neq 0$ for $0\leq j\leq k$.
Hence

$\displaystyle o^{\prime}=$ $\displaystyle\Pi_{j=0}^{k}s_{j}\times r_{z}$
$\displaystyle=$ $\displaystyle s\times
m_{0}\times\Pi_{j=0}^{k}(\Pi_{\ell=1}^{k_{j}}s^{j}_{\ell}\times\Pi_{i=1}^{k_{j}}(m_{S\sqsubseteq
P^{j}_{i}}\times m_{\exists\mathsf{inv}(P_{i}^{j}).A^{j}_{i}\sqsubseteq
B^{j}_{i}})\times\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq{B^{\prime}}^{j}_{i}}\times
p_{j})\times r_{z}$ $\displaystyle=$ $\displaystyle s\times m_{0}$
$\displaystyle\times\Pi_{j=0}^{k}\Pi_{\ell=1}^{k_{j}}s^{j}_{\ell}\times\Pi_{j=0}^{k}\Pi_{i=1}^{k_{j}}(m_{S\sqsubseteq
P^{j}_{i}}\times m_{\exists\mathsf{inv}(P_{i}^{j}).A^{j}_{i}\sqsubseteq
B^{j}_{i}})\times\Pi_{j=0}^{k}\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq{B^{\prime}}^{j}_{i}}$
$\displaystyle\times\Pi_{j=0}^{k}p_{j}\times r_{z}$ $\displaystyle=$
$\displaystyle s\times
m_{0}\times\Pi_{j=0}^{k}\Pi_{\ell=1}^{k_{j}}s^{j}_{\ell}\times\Pi_{j=0}^{k}\Pi_{i=1}^{k_{j}}(m_{S\sqsubseteq
P^{j}_{i}}\times m_{\exists\mathsf{inv}(P_{i}^{j}).A^{j}_{i}\sqsubseteq
B^{j}_{i}})\times\Pi_{j=0}^{k}\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq{B^{\prime}}^{j}_{i}}\times
p$ $\displaystyle=$ $\displaystyle s\times
m_{0}\times\Pi_{\ell=1}^{K}s_{\ell}\times\Pi_{i=1}^{K}(m_{S\sqsubseteq
P_{i}}\times m_{\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq
B_{i}})\times\Pi_{i=1}^{K^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p.$

In the case $K=0$, $k_{j}=0$ for every $0\leq j\leq k$. Hence

$\displaystyle o^{\prime}=$ $\displaystyle\Pi_{j=0}^{k}s_{j}\times r_{z}$
$\displaystyle=$
$\displaystyle\Pi_{j=0}^{k}\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq{B^{\prime}}^{j}_{i}}\times
p_{j}\times r_{z}$ $\displaystyle=$
$\displaystyle\Pi_{j=0}^{k}\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq{B^{\prime}}^{j}_{i}}\times
p$ $\displaystyle=$ $\displaystyle\Pi_{i=1}^{K^{\prime}}m_{\top\sqsubseteq
B^{\prime}_{i}}\times p.$

This shows the property in case (ii) and finishes the proof of the lemma. ∎

######  Lemma B.12.

For all $i\geq 0$, $x,y\in\Delta^{\mathcal{I}_{\mathcal{O}}}$, $R$ role name
or inverse role, and $A\in{\sf N_{C}}\cup\\{\top\\}$, if $(x,y,o)\in
R^{\mathcal{I}_{i}}$, $(y,o^{\prime})\in A^{\mathcal{I}_{i}}$, $(\exists
R.A\sqsubseteq B,n)\in\mathcal{O}$, and $y\notin{\sf N_{I}}$ has been
introduced between $\mathcal{I}_{j-1}$ and $\mathcal{I}_{j}$ ($j\leq i$), to
satisfy an inclusion of the form $(C\sqsubseteq\exists S,m_{0})\in\mathcal{O}$
by applying $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ to some $(x,s)\in
C^{\mathcal{I}_{j-1}}$, then

  * •

there exists $(C\sqcap A_{1}\sqcap\dots\sqcap A_{k}\sqsubseteq
B,r)\in\mathsf{saturate}(\mathcal{O})$ for some $k\geq 0$, such that for every
$1\leq\ell\leq k$, $(x,s_{\ell})\in A_{\ell}^{\mathcal{I}_{i}}$,

  * •

and $s\times\Pi_{\ell=1}^{k}s_{\ell}\times r=o\times o^{\prime}\times n$.

###### Proof.

By Lemma B.10, there exists $(S\sqsubseteq R,m_{S\sqsubseteq
R})\in\mathsf{saturate}(\mathcal{O})$ such that

$s\times m_{0}\times m_{S\sqsubseteq R}=o,$

and by Lemma B.11, the following statements hold.

  1. 1.

There exist $k\geq 0$ and $k^{\prime}\geq 0$ such that:

     * •

$(S\sqsubseteq P_{i},m_{S\sqsubseteq P_{i}})$ and
$(\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq
B_{i},m_{\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq
B_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k$,

     * •

$(\top\sqsubseteq B^{\prime}_{i},m_{\top\sqsubseteq
B^{\prime}_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k^{\prime}$,

     * •

$(B_{1}\sqcap\dots\sqcap B_{k}\sqcap B^{\prime}_{1}\sqcap\dots\sqcap
B^{\prime}_{k^{\prime}}\sqsubseteq A,p)\in\mathsf{saturate}(\mathcal{O})$.

Moreover, if $A=\top$, then $k=k^{\prime}=0$ and $p=1$ (recall that the empty
conjunction is $\top$ and
$(\top\sqsubseteq\top,1)\in\mathsf{saturate}(\mathcal{O})$).

  2. 2.

For every $1\leq\ell\leq k$, there exists $(x,s_{\ell})\in
A_{\ell}^{\mathcal{I}_{i-1}}$.

  3. 3.

The monomials are related as follows:

     * •

If $k\neq 0$, $s\times
m_{0}\times\Pi_{\ell=1}^{k}s_{\ell}\times\Pi_{i=1}^{k}(m_{S\sqsubseteq
P_{i}}\times m_{\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p=o^{\prime}$.

     * •

If $k=0$, $\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p=o^{\prime}$.

Hence, if $(\exists R.A\sqsubseteq B,n)\in\mathcal{O}$, since
$(C\sqsubseteq\exists S,m_{0})\in\mathcal{O}$, it follows by
$\mathsf{CR}^{T}_{3}$ that $(C\sqcap A_{1}\sqcap\dots\sqcap A_{k}\sqsubseteq
B,r)\in\mathsf{saturate}(\mathcal{O})$ with

$r=m_{0}\times n\times m_{S\sqsubseteq R}\times\Pi_{i=1}^{k}(m_{S\sqsubseteq
P_{i}}\times m_{\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p,$

so that

$\displaystyle s\times\Pi_{\ell=1}^{k}s_{\ell}\times r$ $\displaystyle=$
$\displaystyle s\times\Pi_{\ell=1}^{k}s_{\ell}\times m_{0}\times n\times
m_{S\sqsubseteq R}\times\Pi_{i=1}^{k}(m_{S\sqsubseteq P_{i}}\times
m_{\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times p$
$\displaystyle=$ $\displaystyle m_{S\sqsubseteq R}\times s\times
m_{0}\times\Pi_{\ell=1}^{k}s_{\ell}\times\Pi_{i=1}^{k}(m_{S\sqsubseteq
P_{i}}\times m_{\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p\times n$ $\displaystyle=$ $\displaystyle o\times o^{\prime}\times n.\qed$

We are now ready to prove our theorem.

See 4.7

###### Proof.

(1) Point (1) is a special case of Lemma B.8.

(2) Assume that $\mathcal{O}$ is satisfiable and let $\alpha$ be an assertion
and $m$ a monomial. We show that if $\mathcal{O}\models(\alpha,m)$ then
$(\alpha,m)\in\mathsf{saturate}(\mathcal{O})$ by contrapositive: assuming that
$(\alpha,{m})\notin\mathsf{saturate}(\mathcal{O})$, we show that the canonical
model $\mathcal{I}_{\mathcal{O}}=\bigcup_{i\geq 0}\mathcal{I}_{i}$ of
$\mathcal{O}$ (cf. Figure 2) is such that
$\mathcal{I}_{\mathcal{O}}\not\models(\alpha,m)$. We show by induction that
for every $i$, for every assertion $\beta$ and every monomial $m$, if
$(\beta,{m})\notin\mathsf{saturate}(\mathcal{O})$, then
$\mathcal{I}_{i}\not\models(\beta,m)$.

For $i=0$, since $(\beta,{m})\notin\mathsf{saturate}(\mathcal{O})$ implies
$(\beta,{m})\notin\mathcal{O}$, then $\mathcal{I}_{0}\not\models(\beta,m)$ by
construction of $\mathcal{I}_{0}$.

Assume that the property holds for $i\geq 0$ and let $(\beta,m)$ be such that
$(\beta,{m})\notin\mathsf{saturate}(\mathcal{O})$. Assume for a contradiction
that $\mathcal{I}_{i+1}\models(\beta,m)$. Since $\beta$ is an assertion, it is
of the form $S(a,b)$ or $B(a)$ with $S\in{\sf N_{R}}$, $B\in{\sf N_{C}}$ and
$a,b\in{\sf N_{I}}$. Since $\mathcal{I}_{i}\not\models(\beta,m)$ by the
induction hypothesis, it follows that $\mathcal{I}_{i+1}$ has been obtained
from $\mathcal{I}_{i}$ by applying a rule from $\mathsf{R}_{1}$ to
$\mathsf{R}_{5}$ (since the tuples added by $\mathsf{R}_{6}$ and
$\mathsf{R}_{7}$ involve at least one domain element
$x\in\Delta^{\mathcal{I}}\setminus{\sf N_{I}}$). We next show that in every
case, $(\beta,{m})\in\mathsf{saturate}(\mathcal{O})$.

  * •

If $\mathsf{R}_{1}$ has been applied: $(\beta,m)=(S(a,b),o\times n)$ and it
holds that $\mathcal{I}_{i}\models(R(a,b),o)$ and $(R\sqsubseteq
S,n)\in\mathcal{O}$. By induction hypothesis, since
$\mathcal{I}_{i}\models(R(a,b),o)$, then
$(R(a,b),o)\in\mathsf{saturate}(\mathcal{O})$. Hence, it follows from the
construction of $\mathsf{saturate}(\mathcal{O})$ (by $\mathsf{CR}^{A}_{4}$)
that $(\beta,m)\in\mathsf{saturate}(\mathcal{O})$.

  * •

If $\mathsf{R}_{2}$ has been applied: $(\beta,m)=(S(a,b),o\times n)$ and it
holds that $\mathcal{I}_{i}\models(R(b,a),o)$ and $(R\sqsubseteq
S^{-},n)\in\mathcal{O}$. By induction hypothesis, since
$\mathcal{I}_{i}\models(R(b,a),o)$, then
$(R(b,a),o)\in\mathsf{saturate}(\mathcal{O})$. Hence, it follows from the
construction of $\mathsf{saturate}(\mathcal{O})$ (by $\mathsf{CR}^{A}_{5}$)
that $(\beta,m)\in\mathsf{saturate}(\mathcal{O})$.

  * •

If $\mathsf{R}_{3}$ has been applied: $(\beta,m)=(B(a),o_{1}\times o_{2}\times
n)$ and it holds that $\mathcal{I}_{i}\models(A_{1}(a),o_{1})$,
$\mathcal{I}_{i}\models(A_{2}(a),o_{2})$ and $(A_{1}\sqcap A_{2}\sqsubseteq
B,n)\in\mathcal{O}$. By induction hypothesis, since
$\mathcal{I}_{i}\models(A_{j}(a),o_{j})$ for $1\leq j\leq 2$, then
$(A_{j}(a),o_{j})\in\mathsf{saturate}(\mathcal{O})$. Hence, it follows from
the construction of $\mathsf{saturate}(\mathcal{O})$ (by
$\mathsf{CR}^{A}_{1}$) that $(\beta,m)\in\mathsf{saturate}(\mathcal{O})$.

  * •

If $\mathsf{R}_{4}$ has been applied: $(\beta,m)=(B(a),o\times
o^{\prime}\times n)$ and it holds that $\mathcal{I}_{i}\models(R(a,x),o)$,
$\mathcal{I}_{i}\models(A(x),o^{\prime})$, and $(\exists R.A\sqsubseteq
B,n)\in\mathcal{O}$.

If $x\in{\sf N_{I}}$, by induction hypothesis, since
$\mathcal{I}_{i}\models(R(a,x),o)$ and
$\mathcal{I}_{i}\models(A(x),o^{\prime})$, then
$(R(a,x),o)\in\mathsf{saturate}(\mathcal{O})$ and
$(A(x),o^{\prime})\in\mathsf{saturate}(\mathcal{O})$. Hence, it follows from
the construction of $\mathsf{saturate}(\mathcal{O})$ (by
$\mathsf{CR}^{A}_{2}$) that $(\beta,m)\in\mathsf{saturate}(\mathcal{O})$.

Otherwise, if $x\notin{\sf N_{I}}$, $x$ has been introduced during the
construction of $\mathcal{I}_{i}$, let us say between $\mathcal{I}_{j-1}$ and
$\mathcal{I}_{j}$ (with $j\leq i$), to satisfy an inclusion of the form
$(C\sqsubseteq\exists S,m_{0})$ that belongs to $\mathcal{O}$, when applying
$\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ ($S$ can be a role name or an inverse
role). In this case, there exists a monomial $s$ such that $(a,s)\in
C^{\mathcal{I}_{j-1}}$ to which $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ has been
applied to add $(a,x,s\times m_{0})$ to $S^{\mathcal{I}_{j-1}}$, so
$(C(a),s)\in\mathsf{saturate}(\mathcal{O})$ by induction. Moreover, by Lemma
B.12:

    * –

there exists $(C\sqcap A_{1}\sqcap\dots\sqcap A_{k}\sqsubseteq
B,r)\in\mathsf{saturate}(\mathcal{O})$ for some $k\geq 0$, such that for every
$1\leq\ell\leq k$, $(a,s_{\ell})\in A_{\ell}^{\mathcal{I}_{i}}$, so by
induction $(A_{\ell}(a),s_{\ell})\in\mathsf{saturate}(\mathcal{O})$,

    * –

and $s\times\Pi_{\ell=1}^{k}s_{\ell}\times r=o\times o^{\prime}\times n=m$.

Hence, $(\beta,{m})\in\mathsf{saturate}(\mathcal{O})$ by
$\mathsf{CR}_{1}^{A}$.

  * •

The case where $\mathsf{R}_{5}$ has been applied is similar to the case of
$\mathsf{R}_{4}$, using $\mathsf{CR}^{A}_{3}$ instead of $\mathsf{CR}^{A}_{2}$
in the case $x\in{\sf N_{I}}$.

We have thus shown that $(\beta,{m})\in\mathsf{saturate}(\mathcal{O})$
regardless the form of the rule applied between $\mathcal{I}_{i}$ and
$\mathcal{I}_{i+1}$, which contradicts our original assumption. Hence
$\mathcal{I}_{i+1}\not\models(\beta,m)$. We conclude by induction that for
every $(\beta,m)$ such that $(\beta,{m})\notin\mathsf{saturate}(\mathcal{O})$,
$\mathcal{I}_{i}\not\models(\beta,m)$ for every $i\geq 0$, so that
$\mathcal{I}_{\mathcal{O}}\not\models(\beta,m)$. In particular,
$\mathcal{I}_{\mathcal{O}}\not\models(\alpha,m)$ so
$\mathcal{O}\not\models(\alpha,m)$.

(3) Assume that $\mathcal{O}$ is unsatisfiable. We show that there exists
$(\bot(a),n)\in\mathsf{saturate}(\mathcal{O})$ where
$a\in\mathsf{ind}(\mathcal{O})$.

Let $\mathcal{O}^{\prime\prime}$ be the annotated ontology obtained from
$\mathsf{saturate}(\mathcal{O})$ by replacing $\bot$ by a fresh concept name
$\mathit{Bot}$ in the assertions and GCIs, so that $\bot$ only occurs in
negative RIs of $\mathcal{O}^{\prime\prime}$ and let
$\mathcal{O}^{\prime}=\mathcal{O}^{\prime\prime}\cup\mathsf{saturate}(\mathcal{O})$.
Importantly, $\mathsf{saturate}(\mathcal{O}^{\prime})=\mathcal{O}^{\prime}$
since the saturation rules from Table 2 treat $\bot$ in the same way as a
concept name when it occurs in a GCI that appears as a premise of the rule.
Let $\mathcal{I}^{\prime}$ be the canonical model of $\mathcal{O}^{\prime}$.
Since $\mathcal{O}$ is unsatisfiable, then $\mathcal{O}$ does not have any
model. In particular, $\mathcal{I}^{\prime}$ is not a model of $\mathcal{O}$.
Since $\mathcal{O}\subseteq\mathcal{O}^{\prime}$, it follows that
$\mathcal{I}^{\prime}$ does not satisfy a GCI of $\mathcal{O}$ with $\bot$ as
right-hand side or a negative RI of $\mathcal{O}$.

  * •

Case (i): $\mathcal{I}^{\prime}$ does not satisfy a GCI
$(D\sqsubseteq\bot,v)\in\mathcal{O}$, i.e. there exists $(d,m)\in
D^{\mathcal{I}^{\prime}}$. By construction of $\mathcal{O}^{\prime}$,
$(D\sqsubseteq\mathit{Bot},v)\in\mathcal{O}^{\prime}$ so by construction of
$\mathcal{I}^{\prime}$ ($\mathsf{R}_{3}$, $\mathsf{R}_{4}$ or $\mathsf{R}_{5}$
depending on the form of $D$), $(d,m\times
v)\in\mathit{Bot}^{\mathcal{I}^{\prime}}$.

First note that if $d\notin{\sf N_{I}}$, then $d$ has been introduced during
the construction of $\mathcal{I}^{\prime}$, let us say between
$\mathcal{I}^{\prime}_{j-1}$ and $\mathcal{I}^{\prime}_{j}$, to satisfy an
inclusion of the form $(C\sqsubseteq\exists P,m_{0})$ that belongs to
$\mathcal{O}$, when applying $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ with some
$(c,s)\in C^{\mathcal{I}^{\prime}}$.

It is easy to check inductively that there exist
$c_{0}=a\in\mathsf{ind}(\mathcal{O})$ and $c_{1},\dots,c_{k}\notin{\sf N_{I}}$
such that $k\geq 0$, $d=c_{k}$ and each $c_{i}$ has been introduced during the
construction of $\mathcal{I}^{\prime}$ to satisfy an inclusion of the form
$(C_{i}\sqsubseteq\exists P_{i},m_{i})$ that belongs to $\mathcal{O}$, when
applying $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ with $(c_{i-1},s_{i-1})\in
C_{i-1}^{\mathcal{I}^{\prime}}$, so that $(c_{i-1},c_{i},s_{i-1}\times
m_{i})\in P_{i}^{\mathcal{I}^{\prime}}$. We show by induction on $k$ that
$(d,m\times v)\in\mathit{Bot}^{\mathcal{I}^{\prime}}$ implies that there
exists $n$ such that $(\mathit{Bot}(a),n)\in\mathcal{O}^{\prime}$. By
definition of $\mathcal{O}^{\prime}$, it will follow that
$(\bot(a),n)\in\mathsf{saturate}(\mathcal{O})$.

    * –

Base case: $k=0$, i.e. $d=a\in\mathsf{ind}(\mathcal{O})$. Since
$\mathcal{I}^{\prime}\models(\mathit{Bot}(a),m\times v)$, it follows by
Theorem 3.14 that $(\mathit{Bot}(a),m\times v)\in\mathcal{O}^{\prime}$.

    * –

Induction step: Assume that the property is true for $k$ and consider
$(d,m\times v)\in\mathit{Bot}^{\mathcal{I}^{\prime}}$ such that there exists
$c_{0}=a\in\mathsf{ind}(\mathcal{O})$ and $c_{1},\dots,c_{k+1}\notin{\sf
N_{I}}$ such that $d=c_{k+1}$ and each $c_{i}$ has been introduced during the
construction of $\mathcal{I}^{\prime}$ to satisfy an inclusion of the form
$(C_{i}\sqsubseteq\exists P_{i},m_{i})$ that belongs to $\mathcal{O}$, when
applying $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ with $(c_{i-1},s_{i-1})\in
C_{i-1}^{\mathcal{I}^{\prime}}$ so that $(c_{i-1},c_{i},s_{i-1}\times
m_{i})\in P_{i}^{\mathcal{I}^{\prime}}$.

Since $(c_{k},d,s_{k}\times m_{k+1})\in P_{k+1}^{\mathcal{I}^{\prime}}$,
$(d,m\times v)\in\mathit{Bot}^{\mathcal{I}^{\prime}}$, and $(\exists
P_{k+1}.\bot\sqsubseteq\bot,1)\in\mathsf{saturate}(\mathcal{O})$ (by
initialization of $\mathcal{S}$) so that $(\exists
P_{k+1}.\mathit{Bot}\sqsubseteq\mathit{Bot},1)\in\mathcal{O}^{\prime}$, it
follows that $(c_{k},s_{k}\times m_{k+1}\times m\times
v)\in\mathit{Bot}^{\mathcal{I}^{\prime}}$ (by $\mathsf{R}_{4}$ or
$\mathsf{R}_{5}$).

Hence, by induction hypothesis, there exists $n$ such that
$(\mathit{Bot}(a),n)\in\mathcal{O}^{\prime}$.

  * •

Case (ii): $\mathcal{I}^{\prime}$ does not satisfy a RI $(P\sqcap
Q\sqsubseteq\bot,v)\in\mathcal{O}$, i.e. there exists $(c,d,m_{1})\in
P^{\mathcal{I}^{\prime}}$ and $(c,d,m_{2})\in Q^{\mathcal{I}^{\prime}}$.

    * –

If $c,d\in\mathsf{ind}(\mathcal{O})$, since
$\mathcal{I}^{\prime}\models(P(c,d),m_{1})$ and
$\mathcal{I}^{\prime}\models(Q(c,d),m_{2})$, then by Theorem 3.14
$(P(c,d),m_{1})$ and $(Q(c,d),m_{2})$ are in $\mathcal{O}^{\prime}$ hence in
$\mathsf{saturate}(\mathcal{O})$ by construction of $\mathcal{O}^{\prime}$.
Hence, since $(P\sqcap Q\sqsubseteq\bot,v)\in\mathcal{O}$, by
$\mathsf{CR}^{A}_{6}$ or $\mathsf{CR}^{A}_{7}$, $(\bot(c),v\times m_{1}\times
m_{2})\in\mathsf{saturate}(\mathcal{O})$.

    * –

If $c$ or $d$ is not in ${\sf N_{I}}$, assume that $d\notin{\sf N_{I}}$ has
been introduced after $c$ in the construction of $\mathcal{I}^{\prime}$ (the
case where $c$ has been introduced after $d$ is similar). Hence $d$ has been
introduced during the construction of $\mathcal{I}^{\prime}$, let us say
between $\mathcal{I}^{\prime}_{j-1}$ and $\mathcal{I}^{\prime}_{j}$, to
satisfy an inclusion of the form $(C\sqsubseteq\exists S,m_{0})$ or
$(C\sqsubseteq\exists S^{-},m_{0})$ that belongs to $\mathcal{O}$, when
applying $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ respectively. Let us consider
the case $(C\sqsubseteq\exists S,m_{0})$ (the case $(C\sqsubseteq\exists
S^{-},m_{0})$ is similar). We can show that there exist

      * *

$(c,s)\in C^{\mathcal{I}^{\prime}}$,

      * *

$(S\sqsubseteq P,o_{1})\in\mathcal{O}^{\prime}$ hence in
$\mathsf{saturate}(\mathcal{O})$ such that $s\times m_{0}\times o_{1}=m_{1}$,
and

      * *

$(S\sqsubseteq Q,o_{2})\in\mathcal{O}^{\prime}$ hence in
$\mathsf{saturate}(\mathcal{O})$ such that $s\times m_{0}\times o_{2}=m_{2}$.

By $\mathsf{CR}^{T}_{0}$, since $(P\sqcap
Q\sqsubseteq\bot,v)\in\mathsf{saturate}(\mathcal{O})$, it follows that
$(C\sqsubseteq\bot,m_{0}\times o_{1}\times o_{2}\times
v)\in\mathsf{saturate}(\mathcal{O})$. Hence
$(C\sqsubseteq\mathit{Bot},m_{0}\times o_{1}\times o_{2}\times
v)\in\mathcal{O}^{\prime}$ and by the construction of $\mathcal{I}^{\prime}$
($\mathsf{R}_{3}$), $(c,s\times m_{0}\times o_{1}\times o_{2}\times
v)\in\mathit{Bot}^{\mathcal{I}^{\prime}}$, i.e. $(c,m_{1}\times m_{2}\times
v)\in\mathit{Bot}^{\mathcal{I}^{\prime}}$. We can now use the argument of case
(i) to conclude that there exists $a\in\mathsf{ind}(\mathcal{O})$ such that
$(\bot(a),n)\in\mathsf{saturate}(\mathcal{O})$ for some $n$.

It follows that in all cases, there exists
$(\bot(a),n)\in\mathsf{saturate}(\mathcal{O})$ where
$a\in\mathsf{ind}(\mathcal{O})$.

(4) $\mathsf{saturate}(\mathcal{O})$ can be computed in exponential time
w.r.t. the size of $\mathcal{O}$. Indeed, every annotated axiom
$(\alpha,m)\in\mathsf{saturate}(\mathcal{O})\setminus\\{\mathcal{O}\\}$ is
such that $m$ has at most $|\mathcal{O}|$ variables (since $\times$ is
idempotent), so the number of possible $m$ is exponential in the size of
$\mathcal{O}$, and $\alpha$ is of one of the following form:

  * •

a concept or role assertion built from individual names and predicates (or
$\top$ or $\bot$) that occurs in $\mathcal{O}$, and there are polynomially
many such assertions,

  * •

a RI $P_{1}\sqsubseteq P_{2}$ where $P_{1},P_{2}$ or their inverses occur in
$\mathcal{O}$, and there are polynomially many such RIs,

  * •

a negative RI $P_{1}\sqcap P_{2}\sqsubseteq\bot$ or a GCI of the form $\exists
P.\bot\sqsubseteq\bot$ where $P_{1},P_{2}$ or their inverses occur in
$\mathcal{O}$, and there are polynomially many such axioms,

  * •

a GCI $A_{1}\sqcap\dots\sqcap A_{k}\sqsubseteq B$, where $A_{1},\dots,A_{k}$
are concept names that occur in $\mathcal{O}$ (or $k=1$ and $A_{1}=\top$) and
$B$ is a concept name that occurs in $\mathcal{O}$ or $\bot$. Moreover, there
is no repetition among the $A_{i}$ and there is no two GCIs such that one can
be obtained from the other by re-ordering the $A_{i}$ since conjunctions are
treated as sets by the completion rules and written in the lexicographic
order. Hence the number of such GCIs is exponential in the number of concept
names that occur in $\mathcal{O}$.

Hence, in the worst case, $\mathsf{saturate}(\mathcal{O})$ adds to
$\mathcal{O}$ an exponential number of axioms where each axiom may be
annotated with an exponential number of monomials. The total number of
annotated axioms added is thus at most exponential in the size of
$\mathcal{O}$ (there are $O(exp(2|\mathcal{O}|))$ possible annotated axioms).
Since each rule application adds an annotated axiom, it follows that the
algorithm runs in exponential time. ∎

##### Proof of Theorem 4.11

Recall that we say that $\mathcal{O}$ belongs to
$\mathcal{ELHI_{\bot}^{\mathit{restr}}}$ if $\mathcal{O}$ is an ${\cal
E\\!LHI}_{\bot}$ ontology in normal form such that for every role or inverse
role $P$, if there exists $C\in{\sf N_{C}}$ and such that $\mathcal{O}\models
C\sqsubseteq\exists P$ and $\exists\mathsf{inv}(P).A\sqsubseteq
B\in\mathcal{O}$, then $A=\top$. In this case, we modify the completion
algorithm by restricting the rules from Table 2 that may introduce
exponentially many axioms, and add two additional rules $\mathsf{CR}^{T}_{4}$
and $\mathsf{CR}^{T}_{5}$ (see Section 4.1.3).

We show the following lemmas, which are the counterparts of Lemmas B.11 and
B.12 for the $\mathcal{ELHI_{\bot}^{\mathit{restr}}}$. We consider a
$\sf{Why}[{\sf X}]$-annotated $\mathcal{ELHI_{\bot}^{\mathit{restr}}}$
ontology $\mathcal{O}$, its canonical model
$\mathcal{I}_{\mathcal{O}}=\bigcup_{i\geq 0}\mathcal{I}_{i}$ (cf. Figure 2)
and the set $\mathsf{saturate}(\mathcal{O})$ obtained from $\mathcal{O}$ using
the modified completion rules of Section 4.1.3.

######  Lemma B.13.

For all $i\geq 0$, $x,y\in\Delta^{\mathcal{I}_{\mathcal{O}}}$ and $A\in{\sf
N_{C}}\cup\\{\top\\}$ if $(y,o^{\prime})\in A^{\mathcal{I}_{i}}$ and
$y\notin{\sf N_{I}}$ has been introduced between $\mathcal{I}_{j-1}$ and
$\mathcal{I}_{j}$ ($j\leq i$) to satisfy an inclusion of the form
$(C\sqsubseteq\exists S,m_{0})\in\mathcal{O}$ by applying $\mathsf{R}_{6}$ or
$\mathsf{R}_{7}$ to some $(x,s)\in C^{\mathcal{I}_{j-1}}$, then the following
holds.

  1. 1.

There exist $k\geq 0$ and $k^{\prime}\geq 0$ such that $k+k^{\prime}\leq 2$
and:

     * •

$(S\sqsubseteq P_{i},m_{S\sqsubseteq P_{i}})$ and
$(\exists\mathsf{inv}(P_{i}).\top\sqsubseteq
B_{i},m_{\exists\mathsf{inv}(P_{i}).\top\sqsubseteq
B_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k$,

     * •

$(\top\sqsubseteq B^{\prime}_{i},m_{\top\sqsubseteq
B^{\prime}_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k^{\prime}$,

     * •

$(B_{1}\sqcap\dots\sqcap B_{k}\sqcap B^{\prime}_{1}\sqcap\dots\sqcap
B^{\prime}_{k^{\prime}}\sqsubseteq A,p)\in\mathsf{saturate}(\mathcal{O})$
(note that the conjunction contains at most two concept names since
$k+k^{\prime}\leq 2$).

Moreover, if $A=\top$, then $k=k^{\prime}=0$ and $p=1$ (recall that the empty
conjunction is $\top$ and
$(\top\sqsubseteq\top,1)\in\mathsf{saturate}(\mathcal{O})$).

  2. 2.

The monomials are related as follows:

     * •

If $k\neq 0$, $s\times m_{0}\times\Pi_{i=1}^{k}(m_{S\sqsubseteq P_{i}}\times
m_{\exists\mathsf{inv}(P_{i}).\top\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p=o^{\prime}$.

     * •

If $k=0$, $\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p=o^{\prime}$.

###### Proof.

The proof is by induction on $l=i-j$. In the case where $A=\top$, the property
trivially holds with $k=k^{\prime}=0$ for every $l\geq 0$.

_Base case._ In the case where $A\neq\top$, the base case is $l=1$ and is
exactly as in the proof of Lemma B.11.

_Induction step._ Assume that the property is true for every integer up to $l$
and consider the case where $i-j=l+1$. Let
$x,y\in\Delta^{\mathcal{I}_{\mathcal{O}}}$, and assume that $(y,o^{\prime})\in
A^{\mathcal{I}_{i}}$, and $y\notin{\sf N_{I}}$ has been introduced between
$\mathcal{I}_{j-1}$ and $\mathcal{I}_{j}$, to satisfy $(C\sqsubseteq\exists
S,m_{0})\in\mathcal{O}$ by applying $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ to
$(x,s)\in C^{\mathcal{I}_{j-1}}$ (thus adding $(x,y,s\times m_{0})\in
S^{\mathcal{I}_{j}}$). We make a case analysis on the last rule applied to add
$(y,o^{\prime})\in A^{\mathcal{I}_{i}}$.

$\bullet$ Case $\boldsymbol{(y,o^{\prime})\in A^{\mathcal{I}_{i}}}$ added by
applying $\boldsymbol{\mathsf{R}_{3}}$ with $\boldsymbol{(D_{1}\sqcap
D_{2}\sqsubseteq A,m_{D_{1}\sqcap D_{2}\sqsubseteq A})\in\mathcal{O}}$. There
are $(y,o_{1})\in D_{1}^{\mathcal{I}_{i-1}}$ and $(y,o_{2})\in
D_{2}^{\mathcal{I}_{i-1}}$ and $o^{\prime}=m_{D_{1}\sqcap D_{2}\sqsubseteq
A}\times o_{1}\times o_{2}$. For $j\in\\{1,2\\}$, since $(y,o_{j})\in
D_{j}^{\mathcal{I}_{i-1}}$, by induction hypothesis:

  * •

There exist $k_{j}\geq 0$ and $k_{j}^{\prime}\geq 0$ such that
$k_{j}+k^{\prime}_{j}\leq 2$ and:

    * –

$(S\sqsubseteq P^{j}_{i},m_{S\sqsubseteq P^{j}_{i}})$,
$(\exists\mathsf{inv}(P_{i}^{j}).\top\sqsubseteq
B^{j}_{i},m_{\exists\mathsf{inv}(P_{i}^{j}).\top\sqsubseteq
B^{j}_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k_{j}$,

    * –

$(\top\sqsubseteq B^{\prime j}_{i},m_{\top\sqsubseteq B^{\prime
j}_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k_{j}^{\prime}$,

    * –

$(B^{j}_{1}\sqcap\dots\sqcap B^{j}_{k_{j}}\sqcap B^{\prime
j}_{1}\sqcap\dots\sqcap B^{\prime j}_{k_{j}^{\prime}}\sqsubseteq
D_{j},p_{j})\in\mathsf{saturate}(\mathcal{O})$.

  * •

The monomials are related as follows

    * –

If $k_{j}\neq 0$, $s\times m_{0}\times\Pi_{i=1}^{k_{j}}(m_{S\sqsubseteq
P^{j}_{i}}\times m_{\exists\mathsf{inv}(P_{i}^{j}).\top\sqsubseteq
B^{j}_{i}})\times\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq B^{\prime
j}_{i}}\times p_{j}=o_{j}$.

    * –

If $k_{j}=0$, $\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq B^{\prime
j}_{i}}\times p_{j}=o_{j}$.

It follows that for $j\in\\{1,2\\}$:

  * •

If $k_{j}\geq 1$: since $(S\sqsubseteq P^{j}_{i},m_{S\sqsubseteq
P^{j}_{i}})\in\mathsf{saturate}(\mathcal{O})$, then by Lemma B.9,
$(\mathsf{inv}(S)\sqsubseteq\mathsf{inv}(P^{j}_{i}),m_{S\sqsubseteq
P^{j}_{i}})\in\mathsf{saturate}(\mathcal{O})$. Thus, since
$(\exists\mathsf{inv}(P_{i}^{j}).\top\sqsubseteq
B^{j}_{i},m_{\exists\mathsf{inv}(P_{i}^{j}).\top\sqsubseteq B^{j}_{i}})$,
$(\top\sqsubseteq B^{\prime j}_{i},m_{\top\sqsubseteq B^{\prime j}_{i}})$, and
$(B^{j}_{1}\sqcap\dots\sqcap B^{j}_{k_{j}}\sqcap B^{\prime
j}_{1}\sqcap\dots\sqcap B^{\prime j}_{k_{j}^{\prime}}\sqsubseteq D_{j},p_{j})$
are in $\mathsf{saturate}(\mathcal{O})$ (recall that $k_{j}+k^{\prime}_{j}\leq
2$), then by $\mathsf{CR}^{T}_{4}$, $(\exists\mathsf{inv}(S).\top\sqsubseteq
D_{j},m_{\exists\mathsf{inv}(S).\top\sqsubseteq
D_{j}})\in\mathsf{saturate}(\mathcal{O})$ where
$m_{\exists\mathsf{inv}(S).\top\sqsubseteq
D_{j}}=\Pi_{i=1}^{k_{j}}(m_{S\sqsubseteq P^{j}_{i}}\times
m_{\exists\mathsf{inv}(P_{i}^{j}).\top\sqsubseteq
B^{j}_{i}})\times\Pi_{i=1}^{k^{\prime}_{j}}m_{\top\sqsubseteq B^{\prime
j}_{i}}\times p_{j}$.

  * •

If $k_{j}=0$: since $(\top\sqsubseteq B^{\prime j}_{i},m_{\top\sqsubseteq
B^{\prime j}_{i}})$, $1\leq i\leq k_{j}^{\prime}$, and $(B^{\prime
j}_{1}\sqcap\dots\sqcap B^{\prime j}_{k_{j}^{\prime}}\sqsubseteq D_{j},p_{j})$
are in $\mathsf{saturate}(\mathcal{O})$ (recall that $k^{\prime}_{j}\leq 2$),
then by $\mathsf{CR}^{T}_{5}$, $(\top\sqsubseteq D_{j},m_{\top\sqsubseteq
D_{j}})\in\mathsf{saturate}(\mathcal{O})$ where $m_{\top\sqsubseteq
D_{j}}=\Pi_{i=1}^{k^{\prime}_{j}}m_{\top\sqsubseteq B^{\prime j}_{i}}\times
p_{j}$.

Let $K=0$ if $k_{1}=k_{2}=0$, $K=2$ if $k_{1}\neq 0$ and $k_{2}\neq 0$, and
$K=1$ otherwise, and let $K^{\prime}=2-K$. Note that $K,K^{\prime}\geq 0$ and
$K+K^{\prime}\leq 2$.

Rename $D_{1}$ by $D^{\prime}_{1}$ if $k_{1}=0$, and if $D_{2}\neq\top$,
rename $D_{2}$ by: $D_{1}$ if $k_{1}=0$ and $k_{2}\neq 0$, $D^{\prime}_{1}$ if
$k_{1}\neq 0$ and $k_{2}=0$, and $D^{\prime}_{2}$ if $k_{1}=0$ and $k_{2}=0$.
This shows item 1 of the property:

  * •

$(S\sqsubseteq S,1)$ and $(\exists\mathsf{inv}(S).\top\sqsubseteq
D_{i},m_{\exists\mathsf{inv}(S).\top\sqsubseteq
D_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq K$, (take $P_{i}=S$,
$m_{S\sqsubseteq P_{i}}=1$, and $B_{i}=D_{i}$)

  * •

$(\top\sqsubseteq D^{\prime}_{i},m_{\top\sqsubseteq
D^{\prime}_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq K^{\prime}$,
(take $B^{\prime}_{i}=D^{\prime}_{i}$)

  * •

$(D_{1}\sqcap\dots\sqcap D_{K}\sqcap D^{\prime}_{1}\sqcap\dots\sqcap
D^{\prime}_{K^{\prime}}\sqsubseteq A,p)\in\mathsf{saturate}(\mathcal{O})$
where $D_{1}\sqcap\dots\sqcap D_{K}\sqcap D^{\prime}_{1}\sqcap\dots\sqcap
D^{\prime}_{K^{\prime}}=D_{1}\sqcap D_{2}$ and $p=m_{D_{1}\sqcap
D_{2}\sqsubseteq A}$.

To show item 2 of the property, we observe that if $K\neq 0$ (i.e. $k_{1}\neq
0$ or $k_{2}\neq\emptyset$), then

$\displaystyle o^{\prime}=$ $\displaystyle m_{D_{1}\sqcap D_{2}\sqsubseteq
A}\times o_{1}\times o_{2}$ $\displaystyle=$ $\displaystyle p\times
o_{1}\times o_{2}$ $\displaystyle=$ $\displaystyle p\times s\times
m_{0}\times\Pi_{j=1}^{2}(\Pi_{i=1}^{k_{j}}(m_{S\sqsubseteq P^{j}_{i}}\times
m_{\exists\mathsf{inv}(P_{i}^{j}).\top\sqsubseteq
B^{j}_{i}})\times\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq B^{\prime
j}_{i}}\times p_{j})$ $\displaystyle=$ $\displaystyle s\times m_{0}\times
p\times\Pi_{i=1}^{K}(1\times m_{\exists\mathsf{inv}(S).\top\sqsubseteq
D_{i}})\times\Pi_{i=1}^{K^{\prime}}m_{\top\sqsubseteq D^{\prime}_{i}},$

and if $K=0$ (i.e. $k_{1}=k_{2}=0$ and $K^{\prime}=2$)

$\displaystyle o^{\prime}=m_{D_{1}\sqcap D_{2}\sqsubseteq A}\times o_{1}\times
o_{2}=p\times o_{1}\times
o_{2}=p\times\Pi_{j=1}^{2}(\Pi_{i=1}^{k_{j}^{\prime}}m_{\top\sqsubseteq
B^{\prime j}_{i}}\times p_{j})=p\times\Pi_{i=1}^{K^{\prime}}m_{\top\sqsubseteq
D^{\prime}_{i}}.$

This shows the property in this case.

$\bullet$ Case $\boldsymbol{(y,o^{\prime})\in A^{\mathcal{I}_{i}}}$ added by
applying $\boldsymbol{\mathsf{R}_{4}}$ or $\boldsymbol{\mathsf{R}_{5}}$ with
$\boldsymbol{(\exists P.D\sqsubseteq A,m_{\exists P.D\sqsubseteq
A})\in\mathcal{O}}$. There exist $(y,z,o_{yz})\in P^{\mathcal{I}_{i-1}}$ and
$(z,o_{z})\in D^{\mathcal{I}_{i-1}}$ such that $o^{\prime}=o_{yz}\times
o_{z}\times m_{\exists P.D\sqsubseteq A}$. We distinguish two subcases:

  1. (i)

either $z=x$,

  2. (ii)

or $z\neq x$, which implies that $z$ has been introduced between
$j^{\prime}-1$ and $j^{\prime}$ ($j\leq j^{\prime}\leq i$) to satisfy an
inclusion of the form $(E_{0}\sqsubseteq\exists S_{z},m_{z})\in\mathcal{O}$ by
applying $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$.

We start with case (i). It holds that $(y,x,o_{yx})\in P^{\mathcal{I}_{i-1}}$,
$(x,o_{x})\in D^{\mathcal{I}_{i-1}}$ and $o^{\prime}=o_{yx}\times o_{x}\times
m_{\exists P.D\sqsubseteq A}$. Since $(y,x,o_{yx})\in P^{\mathcal{I}_{i-1}}$,
i.e. $(x,y,o_{yx})\in\mathsf{inv}(P)^{\mathcal{I}_{i-1}}$,
$(y,1)\in\top^{\mathcal{I}_{i-1}}$ and $y$ has been introduced to satisfy an
inclusion of the form $(C\sqsubseteq\exists S,m_{0})\in\mathcal{O}$ by
applying $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ to $(x,s)\in
C^{\mathcal{I}_{j-1}}$, by Lemma B.10 (whose proof only uses the completion
rule $\mathsf{CR}^{T}_{1}$ which is not modified in the version for
$\mathcal{ELHI_{\bot}^{\mathit{restr}}}$), there exists
$(S\sqsubseteq\mathsf{inv}(P),m_{S\sqsubseteq\mathsf{inv}(P)})\in\mathsf{saturate}(\mathcal{O})$
such that $s\times m_{0}\times m_{S\sqsubseteq\mathsf{inv}(P)}=o_{yx}$.

Since $(C\sqsubseteq\exists S,m_{0})\in\mathcal{O}$ and
$(S\sqsubseteq\mathsf{inv}(P),m_{S\sqsubseteq\mathsf{inv}(P)})\in\mathsf{saturate}(\mathcal{O})$,
and we have shown that the completion algorithm is correct, it holds that
$\mathcal{O}\models C\sqsubseteq\exists\mathsf{inv}(P)$. Hence, since
$(\exists P.D\sqsubseteq A,m_{\exists P.D\sqsubseteq
A})\in\mathsf{saturate}(\mathcal{O})$, it follows that $D=\top$: Indeed, if
$(\exists P.D\sqsubseteq A,m_{\exists P.D\sqsubseteq A})$ has been added by
the completion algorithm, i.e. by $\mathsf{CR}^{T}_{4}$, $D=\top$ by the
definition of $\mathsf{CR}^{T}_{4}$, and otherwise, $(\exists P.D\sqsubseteq
A,m_{\exists P.D\sqsubseteq A})\in\mathcal{O}$ so since $\mathcal{O}$ belongs
to $\mathcal{ELHI_{\bot}^{\mathit{restr}}}$ (note that $C\in{\sf N_{C}}$), it
must be the case that $D=\top$. Since $D=\top$ and $(x,o_{x})\in
D^{\mathcal{I}_{i-1}}$, it must be the case that $o_{x}=1$. This shows the
property in case (i), indeed:

  1. 1.

If we take $k=1$ and $k^{\prime}=0$, it holds that:

     * •

$(S\sqsubseteq\mathsf{inv}(P),m_{S\sqsubseteq\mathsf{inv}(P)})$ and $(\exists
P.\top\sqsubseteq A,m_{\exists P.\top\sqsubseteq
A})\in\mathsf{saturate}(\mathcal{O})$ (take $P_{1}=\mathsf{inv}(P)$,
$B_{1}=A$),

     * •

$(A\sqsubseteq A,1)\in\mathsf{saturate}(\mathcal{O})$ (take $B_{1}=A$ and
$p=1$).

  2. 2.

$o^{\prime}=o_{yx}\times o_{x}\times m_{\exists P.\top\sqsubseteq
A}=o_{yx}\times 1\times m_{\exists P.\top\sqsubseteq A}=s\times m_{0}\times
m_{S\sqsubseteq\mathsf{inv}(P)}\times m_{\exists P.\top\sqsubseteq A}\times
p.$

We now consider case (ii): $(y,z,o_{yz})\in P^{\mathcal{I}_{i-1}}$,
$(z,o_{z})\in D^{\mathcal{I}_{i-1}}$, $o^{\prime}=o_{yz}\times o_{z}\times
m_{\exists P.D\sqsubseteq A}$ and $z$ has been introduced between
$j^{\prime}-1$ and $j^{\prime}$ ($j\leq j^{\prime}\leq i$) by applying
$\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ to satisfy an inclusion of the form
$(E_{0}\sqsubseteq\exists S_{z},m_{z})\in\mathcal{O}$. There must exist a
monomial $s_{0}$ such that $(y,s_{0})\in E_{0}^{\mathcal{I}_{j^{\prime}-1}}$
to which $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ has been applied. Hence by Lemma
B.10 there exists $(S_{z}\sqsubseteq P,m_{S_{z}\sqsubseteq
P})\in\mathsf{saturate}(\mathcal{O})$ such that $s_{0}\times m_{z}\times
m_{S_{z}\sqsubseteq P}=o_{yz}$, and by induction hypothesis, the following
statements hold.

  * •

There exist $k\geq 0$ and $k^{\prime}\geq 0$ such that $k+k^{\prime}\leq 2$
and:

    * –

$(S_{z}\sqsubseteq P_{i},m_{S_{z}\sqsubseteq P_{i}})$ and
$(\exists\mathsf{inv}(P_{i}).\top\sqsubseteq
B_{i},m_{\exists\mathsf{inv}(P_{i}).\top\sqsubseteq
B_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k$,

    * –

$(\top\sqsubseteq B^{\prime}_{i},m_{\top\sqsubseteq
B^{\prime}_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k^{\prime}$,

    * –

$(B_{1}\sqcap\dots\sqcap B_{k}\sqcap B^{\prime}_{1}\sqcap\dots\sqcap
B^{\prime}_{k^{\prime}}\sqsubseteq D,p)\in\mathsf{saturate}(\mathcal{O})$.

Since $(\exists P.D\sqsubseteq A,m_{\exists P.D\sqsubseteq A})\in\mathcal{O}$
and $(E_{0}\sqsubseteq\exists S_{z},m_{z})\in\mathcal{O}$, it follows by the
modified version of $\mathsf{CR}^{T}_{3}$ that $(E_{0}\sqsubseteq
A,r_{z})\in\mathsf{saturate}(\mathcal{O})$ with $r_{z}=m_{z}\times m_{\exists
P.D\sqsubseteq A}\times m_{S_{z}\sqsubseteq
P}\times\Pi_{i=1}^{k}(m_{S_{z}\sqsubseteq P_{i}}\times
m_{\exists\mathsf{inv}(P_{i}).\top\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p$.

  * •

The monomials are related as follows

    * –

If $k\neq 0$, $s_{0}\times m_{z}\times\Pi_{i=1}^{k}(m_{S_{z}\sqsubseteq
P_{i}}\times m_{\exists\mathsf{inv}(P_{i}).\top\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p=o_{z}$.

    * –

If $k=0$, $\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p=o_{z}$.

Moreover since $(y,s_{0})\in E_{0}^{\mathcal{I}_{i-1}}$, by induction
hypothesis:

  * •

There exist $k_{0}\geq 0$ and $k_{0}^{\prime}\geq 0$ such that
$k_{0}+k_{0}^{\prime}\leq 2$ and:

    * –

$(S\sqsubseteq P^{0}_{i},m_{S\sqsubseteq P^{0}_{i}})$,
$(\exists\mathsf{inv}(P_{i}^{0}).\top\sqsubseteq
B^{0}_{i},m_{\exists\mathsf{inv}(P_{i}^{0}).\top\sqsubseteq
B^{0}_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k_{0}$,

    * –

$(\top\sqsubseteq B^{\prime 0}_{i},m_{\top\sqsubseteq B^{\prime
0}_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k_{0}^{\prime}$,

    * –

$(B^{0}_{1}\sqcap\dots\sqcap B^{0}_{k_{0}}\sqcap B^{\prime
0}_{1}\sqcap\dots\sqcap B^{\prime 0}_{k_{0}^{\prime}}\sqsubseteq
E_{0},p_{0})\in\mathsf{saturate}(\mathcal{O})$.

  * •

The monomials are related as follows

    * –

If $k_{0}\neq 0$, $s\times m_{0}\times\Pi_{i=1}^{k_{0}}(m_{S\sqsubseteq
P^{0}_{i}}\times m_{\exists\mathsf{inv}(P_{i}^{0}).\top\sqsubseteq
B^{0}_{i}})\times\Pi_{i=1}^{k_{0}^{\prime}}m_{\top\sqsubseteq{B^{\prime}}^{0}_{i}}\times
p_{0}=s_{0}$.

    * –

If $k_{0}=0$,
$\Pi_{i=1}^{k_{0}^{\prime}}m_{\top\sqsubseteq{B^{\prime}}^{0}_{i}}\times
p_{0}=s_{0}$.

Since $(B^{0}_{1}\sqcap\dots\sqcap B^{0}_{k_{0}}\sqcap B^{\prime
0}_{1}\sqcap\dots\sqcap B^{\prime 0}_{k_{0}^{\prime}}\sqsubseteq E_{0},p_{0})$
(with $k_{0}+k_{0}^{\prime}\leq 2$) and $(E_{0}\sqsubseteq A,r_{z})$ are in
$\mathsf{saturate}(\mathcal{O})$, by $\mathsf{CR}^{T}_{2}$,
$(B^{0}_{1}\sqcap\dots\sqcap B^{0}_{k_{0}}\sqcap B^{\prime
0}_{1}\sqcap\dots\sqcap B^{\prime 0}_{k_{0}^{\prime}}\sqsubseteq A,p_{0}\times
r_{z})\in\mathsf{saturate}(\mathcal{O})$ and this shows item 1 of the
property. To get item 2 of the property, observe that

$\displaystyle o^{\prime}=$ $\displaystyle o_{yz}\times o_{z}\times m_{\exists
P.D\sqsubseteq A}$ $\displaystyle=$ $\displaystyle s_{0}\times m_{z}\times
m_{S_{z}\sqsubseteq P}\times\Pi_{i=1}^{k}(m_{S_{z}\sqsubseteq P_{i}}\times
m_{\exists\mathsf{inv}(P_{i}).\top\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p\times m_{\exists P.D\sqsubseteq A}$

so that if $k_{0}\neq 0$, then

$\displaystyle o^{\prime}=$ $\displaystyle s\times
m_{0}\times\Pi_{i=1}^{k_{0}}(m_{S\sqsubseteq P^{0}_{i}}\times
m_{\exists\mathsf{inv}(P_{i}^{0}).\top\sqsubseteq
B^{0}_{i}})\times\Pi_{i=1}^{k_{0}^{\prime}}m_{\top\sqsubseteq{B^{\prime}}^{0}_{i}}\times
p_{0}$ $\displaystyle\times m_{z}\times m_{S_{z}\sqsubseteq
P}\times\Pi_{i=1}^{k}(m_{S_{z}\sqsubseteq P_{i}}\times
m_{\exists\mathsf{inv}(P_{i}).\top\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p\times m_{\exists P.D\sqsubseteq A}$ $\displaystyle=$ $\displaystyle s\times
m_{0}\times\Pi_{i=1}^{k_{0}}(m_{S\sqsubseteq P^{0}_{i}}\times
m_{\exists\mathsf{inv}(P_{i}^{0}).\top\sqsubseteq
B^{0}_{i}})\times\Pi_{i=1}^{k_{0}^{\prime}}m_{\top\sqsubseteq{B^{\prime}}^{0}_{i}}\times
p_{0}\times r_{z}$

and if $k_{0}=0$, then

$\displaystyle o^{\prime}=$
$\displaystyle\Pi_{i=1}^{k_{0}^{\prime}}m_{\top\sqsubseteq{B^{\prime}}^{0}_{i}}\times
p_{0}$ $\displaystyle\times m_{z}\times m_{S_{z}\sqsubseteq
P}\times\Pi_{i=1}^{k}(m_{S_{z}\sqsubseteq P_{i}}\times
m_{\exists\mathsf{inv}(P_{i}).\top\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p\times m_{\exists P.D\sqsubseteq A}$ $\displaystyle=$
$\displaystyle\Pi_{i=1}^{k_{0}^{\prime}}m_{\top\sqsubseteq{B^{\prime}}^{0}_{i}}\times
p_{0}\times r_{z}$

This shows the property in case (ii) and finishes the proof of the lemma. ∎

######  Lemma B.14.

For all $i\geq 0$, $x,y\in\Delta^{\mathcal{I}_{\mathcal{O}}}$, $R$ role name
or inverse role, and $A\in{\sf N_{C}}\cup\\{\top\\}$, if $(x,y,o)\in
R^{\mathcal{I}_{i}}$, $(y,o^{\prime})\in A^{\mathcal{I}_{i}}$, $(\exists
R.A\sqsubseteq B,n)\in\mathcal{O}$, and $y\notin{\sf N_{I}}$ has been
introduced between $\mathcal{I}_{j-1}$ and $\mathcal{I}_{j}$ ($j\leq i$), to
satisfy an inclusion of the form $(C\sqsubseteq\exists S,m_{0})\in\mathcal{O}$
by applying $\mathsf{R}_{6}$ or $\mathsf{R}_{7}$ to some $(x,s)\in
C^{\mathcal{I}_{j-1}}$, then

  * •

there exists $(C\sqsubseteq B,r)\in\mathsf{saturate}(\mathcal{O})$,

  * •

and $s\times r=o\times o^{\prime}\times n$.

###### Proof.

By Lemma B.10 (whose proof only uses the completion rule $\mathsf{CR}^{T}_{1}$
which is not modified in the version for
$\mathcal{ELHI_{\bot}^{\mathit{restr}}}$), there exists $(S\sqsubseteq
R,m_{S\sqsubseteq R})\in\mathsf{saturate}(\mathcal{O})$ such that

$s\times m_{0}\times m_{S\sqsubseteq R}=o,$

and by Lemma B.13, the following statements hold.

  1. 1.

There exist $k\geq 0$ and $k^{\prime}\geq 0$ such that $k+k^{\prime}\leq 2$
and:

     * •

$(S\sqsubseteq P_{i},m_{S\sqsubseteq P_{i}})$ and
$(\exists\mathsf{inv}(P_{i}).\top\sqsubseteq
B_{i},m_{\exists\mathsf{inv}(P_{i}).\top\sqsubseteq
B_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k$,

     * •

$(\top\sqsubseteq B^{\prime}_{i},m_{\top\sqsubseteq
B^{\prime}_{i}})\in\mathsf{saturate}(\mathcal{O})$, $1\leq i\leq k^{\prime}$,

     * •

$(B_{1}\sqcap\dots\sqcap B_{k}\sqcap B^{\prime}_{1}\sqcap\dots\sqcap
B^{\prime}_{k^{\prime}}\sqsubseteq A,p)\in\mathsf{saturate}(\mathcal{O})$
(note that the conjunction contains at most two concept names since
$k+k^{\prime}\leq 2$).

Moreover, if $A=\top$, then $k=k^{\prime}=0$ and $p=1$ (recall that the empty
conjunction is $\top$ and
$(\top\sqsubseteq\top,1)\in\mathsf{saturate}(\mathcal{O})$).

  2. 2.

The monomials are related as follows:

     * •

If $k\neq 0$, $s\times m_{0}\times\Pi_{i=1}^{k}(m_{S\sqsubseteq P_{i}}\times
m_{\exists\mathsf{inv}(P_{i}).\top\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p=o^{\prime}$.

     * •

If $k=0$, $\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p=o^{\prime}$.

Hence, if $(\exists R.A\sqsubseteq B,n)\in\mathcal{O}$, since
$(C\sqsubseteq\exists S,m_{0})\in\mathcal{O}$, it follows by the modified
version of $\mathsf{CR}^{T}_{3}$ for $\mathcal{ELHI_{\bot}^{\mathit{restr}}}$
that $(C\sqsubseteq B,r)\in\mathsf{saturate}(\mathcal{O})$ with $r=m_{0}\times
n\times m_{S\sqsubseteq R}\times\Pi_{i=1}^{k}(m_{S\sqsubseteq P_{i}}\times
m_{\exists\mathsf{inv}(P_{i}).\top\sqsubseteq
B_{i}})\times\Pi_{i=1}^{k^{\prime}}m_{\top\sqsubseteq B^{\prime}_{i}}\times
p$, so that $s\times r=o\times o^{\prime}\times n$. ∎

See 4.11

###### Proof.

Let $\mathsf{saturate}^{k}(\mathcal{O})$ be the $k$-saturation of
$\mathcal{O}$, i.e. the annotated ontology obtained from $\mathcal{O}$ through
the completion algorithm restricted to monomials of size at most $k$ (i.e.
that have at most $k$ variables). We show (1) that
$\mathsf{saturate}^{k}(\mathcal{O})$ can be computed in polynomial time w.r.t.
the size of $\mathcal{O}$ and exponential time w.r.t. $k$, (2) that when
$\mathcal{O}$ is satisfiable, $\mathsf{saturate}^{k}(\mathcal{O})$ suffices
for deciding entailment of annotated assertions $(\alpha,m)$ where $m$ is a
monomial of size at most $k$, and (3) that the algorithm can be modified by
ignoring the monomials in the annotated axioms to check in polynomial time
whether $\mathcal{O}$ is satisfiable.

It follows that we can first check that $\mathcal{O}$ is satisfiable in
polynomial time, then compute $\mathsf{saturate}^{|m|}(\mathcal{O})$ in
polynomial time w.r.t. the size of $\mathcal{O}$ and exponential time w.r.t.
$|m|$ to decide whether $\mathcal{O}\models(\alpha,m)$.

(1) Every annotated axiom
$(\alpha,m)\in\mathsf{saturate}^{k}(\mathcal{O})\setminus\mathcal{O}$ is such
that $m$ has at most $k$ variables, so the number of possible $m$ is
exponential in $k$ and polynomial w.r.t. $|\mathcal{O}|$, and $\alpha$ is of
one of the following form:

  * •

a concept or role assertion built from individual names and predicates (or
$\top$ or $\bot$) that occurs in $\mathcal{O}$, and there are polynomially
many such assertions,

  * •

a RI $P_{1}\sqsubseteq P_{2}$ where $P_{1},P_{2}$ or their inverses occur in
$\mathcal{O}$, and there are polynomially many such RIs,

  * •

a negative RI $P_{1}\sqcap P_{2}\sqsubseteq\bot$ or a GCI of the form $\exists
P.\bot\sqsubseteq\bot$ where $P_{1},P_{2}$ or their inverses occur in
$\mathcal{O}$, and there are polynomially many such axioms,

  * •

a GCI of the form $B\sqsubseteq D$ or $B_{1}\sqcap B_{2}\sqsubseteq D$ where
$B_{(i)}\in{\sf N_{C}}\cup\\{\top\\}$ and $D\in{\sf N_{C}}\cup\\{\bot\\}$
occur in $\mathcal{O}$ (thanks to the modifications done to
$\mathsf{CR}^{T}_{2}$ and $\mathsf{CR}^{T}_{3}$), and there are polynomially
many such GCIs, or

  * •

a GCI of the form $\exists P.\top\sqsubseteq B$ (introduced by
$\mathsf{CR}^{T}_{4}$) where $P$ is a role name or inverse role and $B\in{\sf
N_{C}}\cup\\{\bot\\}$, and there are polynomially many such GCIs.

Hence, in the worst case, $\mathsf{saturate}^{k}(\mathcal{O})$ adds to
$\mathcal{O}$ a polynomial number of axioms where each axiom may be annotated
with a number of monomials polynomial in the size of $\mathcal{O}$ and
exponential in $k$ ($O(|\mathcal{O}|^{k})$ monomials): the total number of
annotated axiom is thus polynomial in the size of $\mathcal{O}$ and
exponential in $k$.

(2) To show that every $(\alpha,m)\in\mathsf{saturate}^{k}(\mathcal{O})$ is
entailed by $\mathcal{O}$, since the modified version of $\mathsf{CR}^{T}_{2}$
and $\mathsf{CR}^{T}_{3}$ are special cases of the original
$\mathsf{CR}^{T}_{2}$ and $\mathsf{CR}^{T}_{3}$, we only need to show that
adding $\mathsf{CR}^{T}_{4}$ and $\mathsf{CR}^{T}_{5}$ preserves the soundness
of the completion algorithm. This is easy to check (similarly as we do in the
proof of Lemma B.8).

To show that the algorithm is complete, i.e. that if $\mathcal{O}$ is
satisfiable and $\mathcal{O}\models(\alpha,m)$ with $|m|\leq k$, then
$(\alpha,m)\in\mathsf{saturate}^{k}(\mathcal{O})$, we show (i) that if
$\mathcal{O}$ is satisfiable and $\mathcal{O}\models(\alpha,m)$, then
$(\alpha,m)\in\mathsf{saturate}(\mathcal{O})$ obtained with the modified rules
and (ii) that if $|m|\leq k$ and
$(\alpha,m)\in\mathsf{saturate}(\mathcal{O})$, then
$(\alpha,m)\in\mathsf{saturate}^{k}(\mathcal{O})$.

Point (ii) follows from the fact that every annotated axiom added by a rule
application has at least as many variables as the premises of the rule.

For point (i), we can use exactly the same proof as for point (2) of Theorem
4.7 except that we use Lemma B.14 instead of Lemma B.12 (note that
$\mathsf{CR}^{T}_{2}$ and $\mathsf{CR}^{T}_{3}$ are not used in the proof for
point (2) of Theorem 4.7, except for using Lemma B.12, so that our
modifications do not affect the rest of the proof).

(3) Finally, we show that if we ignore the monomial part of the annotated
axioms, the algorithm terminates in polynomial time, producing
$\mathcal{O}^{\prime}$ that contains some $\bot(a)$ iff $\mathcal{O}$ is
unsatisfiable. It is easy to check that
$\mathcal{O}^{\prime}=\\{\alpha\mid(\alpha,m)\in\mathsf{saturate}(\mathcal{O})\\}$.
Moreover, it follows from the proof of point (1) that the algorithm adds a
polynomial number of axioms, hence it terminates in polynomial time. Finally,
we can show as in the proof of point (3) of Theorem 4.7 that
$\mathcal{O}^{\prime}$ contains some $\bot(a)$ iff $\mathcal{O}$ is
unsatisfiable. ∎

###  B.2 Conjunctive Queries over ${\cal E\\!LHI}_{\bot}$ Ontologies

##### Proof of Theorem 4.13

We start with point (4) of Theorem 4.13 by showing that
$\mathsf{Rew}(q,\mathcal{O})$ can be computed in exponential time in
$|\mathcal{O}|$ and $|q|$ using Algorithm 1111In Line 9 of Algorithm 1, we
have $R^{-}(y,x_{0})$ which does not belong to the syntax of CQs. This is just
used in the intermediate steps of the algorithm, since they are replaced by
concept atoms of the form $D(y_{0})$ in the final set of annotated CQs
computed by the algorithm..

Input: a CQ $q$, an ${\cal E\\!LHI}_{\bot}$ ontology $\mathcal{O}$ in normal
form and its saturation $\mathsf{saturate}$($\mathcal{O}$)

Output: a set $\mathsf{Rew}(q,\mathcal{O})$ of pairs of the form $(q^{*},m)$
where $q^{*}$ is a CQ and $m$ a monomial

1 $Result\leftarrow\\{(q,1)\\}$;

2 $Rew\leftarrow\emptyset$;

3 while  _$Rew\neq Result$_ do

4 $Rew\leftarrow Result$;

5 foreach  _$(q_{i},m_{i})\in Rew$_ do /* rewrite $(q_{i},m_{i})$ */

6 foreach  _$x_{0}$ existentially quantified in $q_{i}$ such that there is no
$R(x_{0},x_{0})\in\mathsf{atoms}(q_{i})$_ do /* (S1) */

7 $q^{*}_{i}\leftarrow q_{i}$;

8 foreach  _$R(x_{0},y)\in\mathsf{atoms}(q^{*}_{i})$_ do

9 $q^{*}_{i}\leftarrow
q^{*}_{i}\setminus\\{R(x_{0},y)\\}\cup\\{R^{-}(y,x_{0})\\}$; /* (S2) */

10

11 $V_{p}\leftarrow\\{y\mid Q(y,x_{0})\in q^{*}_{i}\text{ for some }Q\\}$; /*
(S3) */

12 $RoleAt(x_{0})\leftarrow\\{Q(y,x_{0})\mid Q(y,x_{0})\in q^{*}_{i}\\}$;

13 $ConceptAt(x_{0})\leftarrow\\{C(x_{0})\mid C(x_{0})\in q^{*}_{i}\\}$;

14 foreach  _$(A\sqsubseteq\exists P,v)\in\mathcal{O}$_ do /* $A\in{\sf
N_{C}}$ since $\mathcal{O}$ in normal form */

15 $RoleRew\leftarrow\mathsf{RoleAtRew}(q^{*}_{i},x_{0},A\sqsubseteq\exists
P)$; /* Algorithm 2 */

16
$ConceptRew\leftarrow\mathsf{ConceptAtRew}(q^{*}_{i},x_{0},A\sqsubseteq\exists
P)$; /* Algorithm 3 */

17 foreach  _$mon_{r}\in RoleRew$_ do

18 foreach  _$(At,mon_{c})\in ConceptRew$_ do

19 $q^{\prime}_{i}\leftarrow q^{*}_{i}\setminus(RoleAt(x_{0})\cup
ConceptAt(x_{0}))$; /* (S4) */

20 choose $y_{0}\in V_{p}$; /* (S5) */

21 $q^{\prime}_{i}\leftarrow q^{\prime}_{i}[y^{\prime}\leftarrow y_{0}\mid
y^{\prime}\in V_{p}]$;

22 $q^{\prime}_{i}\leftarrow
q^{\prime}_{i}\cup\\{A(y_{0})\\}\cup\\{D(y_{0})\mid D\in At\\}$; /* (S6) */

23 $Result\leftarrow Result\cup\\{(q^{\prime}_{i},m_{i}\times v\times
mon_{r}\times mon_{c})\\}$;

24

25Output $Result$;

ALGORITHM 1 Compute $\mathsf{Rew}(q,\mathcal{O})$

Input: a CQ $q^{*}_{i}$, a variable $x_{0}$, $P\in{\sf N_{R}}$,
$\mathsf{saturate}(\mathcal{O})$

Output: a set $\mathsf{RoleAtRew}(q^{*}_{i},x_{0},A\sqsubseteq\exists P)$ of
monomials

1 $ListMonSets\leftarrow\emptyset$;

2 foreach  _$Q(y,x_{0})\in q^{*}_{i}$_ do

3 $MonSetQ\leftarrow\emptyset$; /* store monomials of RIs that allow to
rewrite $Q$ in $P$ */

4 foreach  _$(P\sqsubseteq Q,m_{P\sqsubseteq
Q})\in\mathsf{saturate}(\mathcal{O})$_ do

5 $MonSetQ\leftarrow MonSetQ\cup\\{m_{P\sqsubseteq Q}\\}$;

6

7 if  _$MonSetQ=\emptyset$_ then /* $Q$ cannot be rewritten into $P$ */

8 Return $\emptyset$;

9 $ListMonSets\leftarrow ListMonSets\cup\\{MonSetQ\\}$

10$Result\leftarrow\\{1\\}$; /* compute all possible products of one monomial
per $Q(y,x_{0})$ */

11 foreach  _$MonSetQ\in ListMonSets$_ do

12 $Res\leftarrow\emptyset$;

13 foreach  _$n_{1}\in Result$_ do

14 foreach  _$n_{2}\in MonSetQ$_ do

15 $Res\leftarrow Res\cup\\{n_{1}\times n_{2}\\}$;

16

17 $Result\leftarrow Res$;

18

19Return $Result$;

ALGORITHM 2 Compute $\mathsf{RoleAtRew}(q^{*}_{i},x_{0},A\sqsubseteq\exists
P)$

Input: a CQ $q^{*}_{i}$, a variable $x_{0}$, $P\in{\sf N_{R}}$,
$\mathsf{saturate}(\mathcal{O})$

Output: a set $\mathsf{ConceptAtRew}(q^{*}_{i},x_{0},A\sqsubseteq\exists P)$
of pairs of the form $(At,m)$ where $At\subseteq{\sf N_{C}}$ and $m$ is a
monomial

1 $ListPairSets\leftarrow\emptyset$;

2 foreach  _$C(x_{0})\in q^{*}_{i}$_ do

3 $PairSetC\leftarrow\emptyset$; /* store pairs $(At,m)$ that correspond to
axioms that allow to rewrite $C$ using $P$ */

4 foreach  _$(B_{1}\sqcap\dots\sqcap B_{p}\sqsubseteq
C,n_{C})\in\mathsf{saturate}(\mathcal{O})$_ do

5 $ListPairSBs\leftarrow\emptyset$;

6 foreach  _$1\leq i\leq p$_ do

7 $PairSB_{i}\leftarrow\emptyset$; /* store pairs $(At,m)$ that correspond to
axioms that allow to rewrite $B_{i}$ using $P$ */

8 foreach  _$(P\sqsubseteq P_{i},m_{i})\in\mathsf{saturate}(\mathcal{O})$_ do

9 foreach  _$(\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq
B_{i},v_{i})\in\mathcal{O}$_ do

10 $PairSB_{i}\leftarrow PairSB_{i}\cup\\{(\\{A_{i}\\},v_{i}\times m_{i})\\}$;

11

12 foreach  _$(\top\sqsubseteq B_{i},o_{i})\in\mathsf{saturate}(\mathcal{O})$_
do

13 $PairSB_{i}\leftarrow PairSB_{i}\cup\\{(\emptyset,o_{i})\\}$;

14

15 $ListPairSBs\leftarrow ListPairSBs\cup\\{PairSB_{i}\\}$;

16

17 $PairSet\leftarrow\\{(\emptyset,n_{C})\\}$; /* compute the part of
$PairSetC$ that uses $(B_{1}\sqcap\dots\sqcap B_{p}\sqsubseteq C,n_{C})$ with
all possible choices of one pair per $B_{i}$ */

18 foreach  _$PairSB_{i}\in ListPairSBs$_ do

19 $Res\leftarrow\emptyset$;

20 foreach  _$(At_{1},n_{1})\in PairSet$_ do

21 foreach  _$(At_{2},n_{2})\in PairSB_{i}$_ do

22 $Res\leftarrow Res\cup\\{(At_{1}\cup At_{2},n_{1}\times n_{2}))\\}$;

23

24 $PairSet\leftarrow Res$;

25

26 $PairSetC\leftarrow PairSetC\cup PairSet$;

27 if  _$PairSetC=\emptyset$_ then /* $C$ cannot be rewritten using $P$ */

28 Return $\emptyset$;

29 $ListPairSets\leftarrow ListPairSets\cup\\{PairSetC\\}$

30$Result\leftarrow\\{(\emptyset,1)\\}$; /* compute all possible products of
one pair per $C(x_{0})$ */

31 foreach  _$PairSetC\in ListPairSets$_ do

32 $Res\leftarrow\emptyset$;

33 foreach  _$(At_{1},n_{1})\in Result$_ do

34 foreach  _$(At_{2},n_{2})\in PairSetC$_ do

35 $Res\leftarrow Res\cup\\{(At_{1}\cup At_{2},n_{1}\times n_{2})\\}$;

36

37 $Result\leftarrow Res$;

38

39Return $Result$;

ALGORITHM 3 Compute $\mathsf{ConceptAtRew}(q^{*}_{i},x_{0},A\sqsubseteq\exists
P)$

######  Lemma B.15.

Algorithm 1 computes $\mathsf{Rew}(q,\mathcal{O})$.

###### Proof.

Let $(q^{*},m)\in\mathsf{Rew}(q,\mathcal{O})$. There exists a rewriting
sequence
$(q_{0},m_{0})\rightarrow_{\mathcal{O}}(q_{1},m_{1})\rightarrow_{\mathcal{O}}\dots\rightarrow_{\mathcal{O}}(q_{k},m_{k})$
where $(q,1)=(q_{0},m_{0})$ and $(q^{*},m)=(q_{k},m_{k})$. We show by
induction that $(q_{i},m_{i})$ is produced by Algorithm 1 for every $0\leq
i\leq k$.

_Base case, $i=0$._ Since Algorithm 1 initializes $Result$ with $\\{(q,1)\\}$
and only adds elements to $Result$, it holds that Algorithm 1 produces
$(q_{0},m_{0})$.

_Induction step._ Assume that Algorithm 1 produces $(q_{i},m_{i})$ and that
$(q_{i},m_{i})\rightarrow_{\mathcal{O}}(q_{i+1},m_{i+1})$, i.e.
$(q_{i+1},m_{i+1})$ is obtained from $(q_{i},m_{i})$ by applying steps (S1) to
(S6) of Definition 4.12. After Algorithm 1 adds $(q_{i},m_{i})$ to $Result$,
$Rew\neq Result$ so the while-loop is entered. Then since $(q_{i},m_{i})\in
Result$, it is considered in the foreach-loop in line 1 of Algorithm 1.

  * •

Let $x_{0}$ be the existentially quantified variable of $q_{i}$ selected in
step (S1): $x_{0}$ fulfills the conditions to be considered in the foreach-
loop in line 1.

  * •

Step (S2) corresponds to lines 1 and 1.

  * •

Let $(A\sqsubseteq\exists P,v)\in\mathcal{O}$ be the GCI selected by step
(S3): $(A\sqsubseteq\exists P,v)$ is considered in the foreach-loop in line 1.
We show that $At(q_{i},x_{0},A\sqsubseteq\exists P)$ and
$mon(q_{i},x_{0},A\sqsubseteq\exists P)$ constructed in step (S3) are such
that there are
$mon_{r}\in\mathsf{RoleAtRew}(q^{*}_{i},x_{0},A\sqsubseteq\exists P)$ and
$(At,mon_{c})\in\mathsf{ConceptAtRew}(q^{*}_{i},x_{0},A\sqsubseteq\exists P)$
such that $At=At(q_{i},x_{0},A\sqsubseteq\exists P)\setminus\\{A\\}$ and
$v\times mon_{r}\times mon_{c}=mon(q_{i},x_{0},A\sqsubseteq\exists P)$. This
follows from the fact that :

    1. 1.

Algorithm 2 returns the set of all monomials that can be obtained as a product
of the form $\prod_{Q(y,x_{0})\in q^{*}_{i}}m_{Q}$ where for each
$Q(y,x_{0})\in q^{*}_{i}$, $m_{Q}\in MonSetQ$ and $MonSetQ=\\{m_{P\sqsubseteq
Q}\mid(P\sqsubseteq Q,m_{P\sqsubseteq
Q})\in\mathsf{saturate}(\mathcal{O})\\}$. In particular, it contains the
product $mon_{r}$ of the $m_{P\sqsubseteq Q}$ selected by step (S3)(a).

    2. 2.

Algorithm 3 returns the set of all pairs $(At,mon_{c})$ that can be obtained
as the union and product of pairs of sets of concept names $At_{C}$ and
monomials $n_{C}\times m_{C}$ for all $C(x_{0})\in q^{*}_{i}$, such that there
is $(B_{1}\sqcap\dots\sqcap B_{p}\sqsubseteq
C,n_{C})\in\mathsf{saturate}(\mathcal{O})$ and for every $1\leq i\leq p$
either there is a pair $(\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq
B_{i},v_{i})\in\mathcal{O}$ and $(P\sqsubseteq
P_{i},m_{i})\in\mathsf{saturate}(\mathcal{O})$ or there is $(\top\sqsubseteq
B_{i},o_{i})\in\mathsf{saturate}(\mathcal{O})$ such that $At_{C}$ is the set
of the $A_{i}$ and $m_{C}$ is the product of the $v_{i}\times m_{i}$ or
$o_{i}$. In particular, some $(At,mon_{c})$ corresponds to the GCIs and RIs
selected by step (S3)(b).

  * •

Finally, step (S4) corresponds to line 1, step (S5) corresponds to lines 1 and
1 and step (S6) corresponds to line 1.

Hence, $(q_{i+1},m_{i+1})$ is in the set $Result$ returned by Algorithm 1.

In the other direction, assume that $(q^{*},m)$ is in the set $Result$
returned by Algorithm 1. Since Algorithm 1 only adds elements to $Result$, we
can prove that there exists a rewriting sequence
$(q_{0},m_{0})\rightarrow_{\mathcal{O}}(q_{1},m_{1})\rightarrow_{\mathcal{O}}\dots\rightarrow_{\mathcal{O}}(q_{k},m_{k})$
where $(q,1)=(q_{0},m_{0})$ and $(q^{*},m)=(q_{k},m_{k})$ by induction on the
number of iterations of the while-loop of Algorithm 1 before it produces
$(q^{*},m)$.

_Base case._ If $(q^{*},m)$ is in the set returned by Algorithm 1 when the
while-loop has not been entered, $(q^{*},m)=(q,1)$ and there exists a
rewriting sequence as required (with $k=0$).

_Induction step._ Assume that every $(q_{i},m_{i})$ produced by Algorithm 1
after $n$ iterations of the while-loop are such that there exists a rewriting
sequence as required. Let $(q_{i+1},m_{i+1})$ be added to $Result$ by
Algorithm 1 in the $n+1$ iteration of the while-loop and $(q_{i},m_{i})\in
Rew$ be the query that corresponds to the for-loop (line 1) in which
$(q_{i+1},m_{i+1})$ is added. It is sufficient to show that
$(q_{i},m_{i})\rightarrow_{\mathcal{O}}(q_{i+1},m_{i+1})$ to conclude by
induction.

  * •

Let $x_{0}$, $(A\sqsubseteq\exists P,v)$, $mon_{r}$, $(At,mon_{c})$ correspond
to the foreach-loops (lines 1, 1, 1, and 1 respectively) in which
$(q_{i+1},m_{i+1})$ is added: it is clear that $x_{0}$ fulfills the conditions
to be selected in step (S1) and we show that $(A\sqsubseteq\exists P,v)$
fulfills those to be selected in step (S3) and that step (S3) can choose
$At(q_{i},x_{0},A\sqsubseteq\exists P)$ and
$mon(q_{i},x_{0},A\sqsubseteq\exists P)$ such that
$At(q_{i},x_{0},A\sqsubseteq\exists P)\setminus\\{A\\}=At$ and
$mon(q_{i},x_{0},A\sqsubseteq\exists P)=v\times mon_{r}\times mon_{c}$.

    1. 1.

Since $mon_{r}\in\mathsf{RoleAtRew}(q^{*}_{i},x_{0},A\sqsubseteq\exists P)$,
Algorithm 2 outputs a non-empty set. Hence for every $Q(y,x_{0})\in
q^{*}_{i}$, $MonSetQ\neq\emptyset$, i.e. there exists $(P\sqsubseteq
Q,m_{P\sqsubseteq Q})\in\mathsf{saturate}(\mathcal{O})$. Moreover, $mon_{r}$
is one of the products built by selecting one such $m_{P\sqsubseteq Q}$ per
$Q(y,x_{0})\in q^{*}_{i}$.

    2. 2.

Since
$(At,mon_{c})\in\mathsf{ConceptAtRew}(q^{*}_{i},x_{0},A\sqsubseteq\exists P)$,
Algorithm 3 outputs a non-empty set. Hence for every $C(x_{0})\in q_{i}$,
$PairSetC\neq\emptyset$, i.e. there exists $(B_{1}\sqcap\dots\sqcap
B_{p}\sqsubseteq C,n_{C})\in\mathsf{saturate}(\mathcal{O})$ such that the
corresponding $PairSet$ is non-empty when added to $PairSetC$. It follows that
for every $1\leq i\leq p$, $PairSB_{i}\neq\emptyset$ (since otherwise
$PairSet$ is replaced by $\emptyset$ in line 3). Finally,
$PairSB_{i}\neq\emptyset$ implies the existence of either $(P\sqsubseteq
P_{i},m_{i})\in\mathsf{saturate}(\mathcal{O})$ and
$(\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq B_{i},v_{i})\in\mathcal{O}$ or
of $(\top\sqsubseteq B_{i},o_{i})\in\mathsf{saturate}(\mathcal{O})$. Moreover,
each $PairSetC$ contains all possible pairs $(At_{C},n_{C}\times m_{C})$ that
correspond to the choice of some $(B_{1}\sqcap\dots\sqcap B_{p}\sqsubseteq
C,n_{C})$ and for $1\leq i\leq p$ of either $(P\sqsubseteq P_{i},m_{i})$ and
$(\exists\mathsf{inv}(P_{i}).A_{i}\sqsubseteq B_{i},v_{i})$ or of
$(\top\sqsubseteq B_{i},o_{i})$, so $(At,mon_{c})$ is one of the pairs built
by selecting one such pair per $C(x_{0})\in q_{i}$ and aggregating them.

  * •

It is then easy to check that step (S2) is performed by lines 1 and 1, step
(S4) by line 1, step (S5) by lines 1 and 1 and step (S6) by line 1.

It follows that we can obtain $(q_{i+1},m_{i+1})$ from $(q_{i},m_{i})$ by
applying steps (S1) to (S6), i.e.
$(q_{i},m_{i})\rightarrow_{\mathcal{O}}(q_{i+1},m_{i+1})$. ∎

######  Lemma B.16.

For every $(q^{*},m)\in\mathsf{Rew}(q,\mathcal{O})$, the size of $(q^{*},m)$
is polynomial w.r.t. $|\mathcal{O}|$ and $|q|$. Hence the cardinality of
$\mathsf{Rew}(q,\mathcal{O})$ is exponential in $|\mathcal{O}|$ and $|q|$.

###### Proof.

For every $(q^{*},m)\in\mathsf{Rew}(q,\mathcal{O})$, since
$\mathsf{terms}(q^{*})\subseteq\mathsf{terms}(q)$ and the atoms of $q^{*}$ use
concept and role names that occur in $\mathcal{O}$, the size of $q^{*}$ is
bounded by $|\mathsf{sig}(\mathcal{O})|\times|\mathsf{terms}(q)|^{2}$. Hence
the size of $q^{*}$ is polynomial w.r.t. $|\mathcal{O}|$ and $|q|$. Moreover,
since $m$ is a product of variables that occur in $\mathcal{O}$, the size of
$m$ is linear w.r.t. $|\mathcal{O}|$.

It follows that the cardinality of
$\\{q^{*}\mid(q^{*},m)\in\mathsf{Rew}(q,\mathcal{O})\\}$ is exponential in
$|\mathcal{O}|$ and $|q|$ and the cardinality of
$\\{m\mid(q^{*},m)\in\mathsf{Rew}(q,\mathcal{O})\\}$ is exponential in
$|\mathcal{O}|$. Hence the cardinality of $\mathsf{Rew}(q,\mathcal{O})$ is
exponential in $|\mathcal{O}|$ and $|q|$. ∎

######  Lemma B.17.

Algorithm 2 runs in exponential time w.r.t. $|q|$ and $|\mathcal{O}|$.

###### Proof.

Every foreach-loop of Algorithm 2 iterates over a set whose size is
exponentially bounded w.r.t. $|\mathcal{O}|$ and $|q|$. In line 2, by Lemma
B.16, the number of atoms in $q^{*}_{i}$ is polynomial w.r.t. $|\mathcal{O}|$
and $|q|$. In line 2, by Theorem 4.7, $\mathsf{saturate}(\mathcal{O})$ can be
computed in exponential time hence is of exponential size w.r.t.
$|\mathcal{O}|$. In line 2, $ListMonSets$ contains a polynomial number
(bounded by the size of $q^{*}_{i}$) of sets $MonSetQ$. In line 2, each set
$MonSetQ$ constructed by the algorithm is a set of monomials from
$\mathsf{saturate}(\mathcal{O})$ hence is of exponential size w.r.t.
$|\mathcal{O}|$. Finally, in line 2, $Result$ is bounded by
$\prod_{Q(y,x_{0})\in q^{*}_{i}}|MonSetQ|$ where $|q^{*}_{i}|$ is polynomial
w.r.t. $|\mathcal{O}|$ and $|q|$ and $|MonSetQ|$ is exponential w.r.t.
$|\mathcal{O}|$, hence $|Result|$ is exponential w.r.t. $|q|$ and
$|\mathcal{O}|$. ∎

######  Lemma B.18.

Algorithm 3 runs in exponential time w.r.t. $|q|$ and $|\mathcal{O}|$.

###### Proof.

Every foreach-loop of Algorithm 3 iterates over a set whose size is
exponentially bounded w.r.t. $|\mathcal{O}|$ and $|q|$. In line 3, by Lemma
B.16, the number of atoms in $q^{*}_{i}$ is polynomial w.r.t. $|\mathcal{O}|$
and $|q|$. In lines 3, 3, 3, 3, by Theorem 4.7,
$\mathsf{saturate}(\mathcal{O})$ can be computed in exponential time hence is
of exponential size w.r.t. $|\mathcal{O}|$. In line 3, for every
$(B_{1}\sqcap\dots\sqcap B_{p}\sqsubseteq
C,n_{C})\in\mathsf{saturate}(\mathcal{O})$, $p$ is bounded by the number of
concept names that occur in $\mathcal{O}$, hence is linear in $|\mathcal{O}|$.
In line 3, each $ListPairSBs$ constructed by the algorithm is a set of $p$
sets for some $(B_{1}\sqcap\dots\sqcap B_{p}\sqsubseteq
C,n_{C})\in\mathsf{saturate}(\mathcal{O})$, so contains a linear number of
sets. In line 3, for each $PairSB_{i}$ constructed by the algorithm,
$PairSB_{i}$ is a set of pairs that consists of a set of 0 or 1 concept name
that occurs in $\mathcal{O}$ and a product of one or two monomials that occur
in $\mathsf{saturate}(\mathcal{O})$, so $|PairSB_{i}|$ is exponential w.r.t.
$|\mathcal{O}|$. In line 3, for each $PairSet$ constructed by the algorithm,
$|PairSet|$ is bounded by $\prod_{i=1}^{p}|PairSetB_{i}|$ where $p$ is linear
w.r.t. $|\mathcal{O}|$ and $|PairSB_{i}|$ is exponential w.r.t.
$|\mathcal{O}|$, hence $|PairSet|$ is exponential w.r.t. $|\mathcal{O}|$. In
line 3, $ListPairSets$ is bounded by the number of atoms $C(x_{0})$ in
$q^{*}_{i}$ so is polynomial w.r.t. $|\mathcal{O}|$ and $|q|$. In line 3, for
each $PairSetC$ constructed by the algorithm, $|PairSetC|$ is bounded by the
number of $(B_{1}\sqcap\dots\sqcap B_{p}\sqsubseteq
C,n_{C})\in\mathsf{saturate}(\mathcal{O})$ so is exponentially bounded w.r.t.
$|\mathcal{O}|$. In line 3, $|Result|$ is bounded by $\prod_{C(x_{0})\in
q^{*}_{i}}|PairSetC|$ where $|q^{*}_{i}|$ is polynomial w.r.t. $|\mathcal{O}|$
and $|q|$ and $|PairSetC|$ is exponential w.r.t. $|\mathcal{O}|$, hence
$|Result|$ is exponential w.r.t. $|q|$ and $|\mathcal{O}|$. ∎

######  Lemma B.19.

Algorithm 1 runs in exponential time w.r.t. $|q|$ and $|\mathcal{O}|$.

###### Proof.

By Lemma B.16, $|\mathsf{Rew}(q,\mathcal{O})|$ is exponential in
$|\mathcal{O}|$ and $|q|$ so Algorithm 1 runs the while-loop an exponential
number of times w.r.t. in $|\mathcal{O}|$ and $|q|$. Moreover, at each
iteration of the while-loop, every foreach-loop iterates over a set whose size
is exponentially bounded w.r.t. $|\mathcal{O}|$ and $|q|$ and each iteration
takes at most exponential time w.r.t. $|\mathcal{O}|$ and $|q|$:

  * •

$|Rew|$ is bounded by $|\mathsf{Rew}(q,\mathcal{O})|$ so exponential w.r.t.
$|\mathcal{O}|$ and $|q|$.

  * •

For each $(q_{i},m_{i})$, by Lemma B.16 $(q_{i},m_{i})$ has polynomial size
w.r.t. $|\mathcal{O}|$ and $|q|$ so both the number of variables in $q_{i}$
and $|\mathsf{atoms}(q^{*}_{i})|$ are polynomial w.r.t. $|\mathcal{O}|$ and
$|q|$.

  * •

By Lemmas B.17 and B.18,
$\mathsf{RoleAtRew}(q^{*}_{i},x_{0},A\sqsubseteq\exists P)$ and
$\mathsf{ConceptAtRew}(q^{*}_{i},x_{0},A\sqsubseteq\exists P)$ are executed in
exponential time w.r.t. $|\mathcal{O}|$ and $|q|$, hence their results
$RoleRew$ and $ConceptRew$ are of exponential size w.r.t. $|\mathcal{O}|$ and
$|q|$.∎

See 4.13

###### Proof.

Claim (4) of the theorem follows from Lemmas B.15 and B.19:
$\mathsf{Rew}(q,\mathcal{O})$ can be computed in exponential time in
$|\mathcal{O}|$ and $|q|$ using Algorithm 1. Moreover, claim (3) implies
claims (1) and (2):

  * •

Since $\sf{Why}[{\sf X}]$ is $\otimes$-idempotent and positive,
$\mathcal{O}^{\prime}\models q(\vec{a})$ iff
$\mathcal{P}(q(\vec{a}),\mathcal{O})\neq 0$ by Theorem 3.19, and claim (3)
implies that $\mathcal{P}(q(\vec{a}),\mathcal{O})\neq 0$ iff there exists
$(q^{*},m^{*})\in\mathsf{Rew}(q,\mathcal{O})$ such that there is a match for
the extended version of $q^{*}(\vec{a})$ in $\mathcal{D}$ (note that all
monomials that occur in $\mathsf{Rew}(q,\mathcal{O})$ are different from 0
since by construction they are products of variables that annotate
$\mathcal{O}$), so iff there exists
$(q^{*},m^{*})\in\mathsf{Rew}(q,\mathcal{O})$ such that there is a match for
$q^{*}(\vec{a})$ in $\mathcal{D}^{\prime}$ (by Proposition 3.7).

  * •

$\mathcal{P}(q(\vec{a}),\mathcal{O})=\sum_{\mathcal{O}\models(q(\vec{a}),m)}m$
so claim ( 3) implies that $\mathcal{O}\models(q(\vec{a}),m)$ iff $m$ occurs
in
$\sum_{(q^{*},m^{*})\in\mathsf{Rew}(q,\mathcal{O})}m^{*}\times\mathcal{P}(q^{*}(\vec{a}),\mathcal{D})=\sum_{(q^{*},m^{*})\in\mathsf{Rew}(q,\mathcal{O})}\sum_{\mathcal{D}\models(q^{*}(\vec{a}),o)}m^{*}\times
o$.

We thus prove claim (3), i.e. that
$\mathcal{P}(q(\vec{a}),\mathcal{O})=\sum_{(q^{*},m^{*})\in\mathsf{Rew}(q,\mathcal{O})}m^{*}\times\mathcal{P}(q^{*}(\vec{a}),\mathcal{D})$.
By definition of the provenance of a query and by Theorem 3.14, it holds that:

  * •

$\mathcal{P}(q(\vec{a}),\mathcal{O})=\sum_{n\in{\sf
prov}_{\mathcal{I}_{\mathcal{O}}}({\boldsymbol{q}(\vec{a})})}n$ where
$\mathcal{I}_{\mathcal{O}}$ is the canonical model of $\mathcal{O}$ and
$\boldsymbol{q}$ the extended version of $q$,

  * •

$\mathcal{P}(q^{*}(\vec{a}),\mathcal{D})=\sum_{o\in{\sf
prov}_{\mathcal{I}_{\mathcal{D}}}({\boldsymbol{q^{*}}(\vec{a})})}o$ where
$\mathcal{I}_{\mathcal{D}}$ is the canonical model of $\mathcal{D}$ and
$\boldsymbol{q^{*}}$ the extended version of $q^{*}$, so that
$\sum_{(q^{*},m^{*})\in\mathsf{Rew}(q,\mathcal{O})}m^{*}\times\mathcal{P}(q^{*}(\vec{a}),\mathcal{D})=\sum_{(q^{*},m^{*})\in\mathsf{Rew}(q,\mathcal{O})}\sum_{o\in{\sf
prov}_{\mathcal{I}_{\mathcal{D}}}({\boldsymbol{q^{*}}(\vec{a})})}m^{*}\times
o$.

We thus need to show that

${\sf
prov}_{\mathcal{I}_{\mathcal{O}}}({\boldsymbol{q}(\vec{a})})=\\{m^{*}\times
o\mid(q^{*},m^{*})\in\mathsf{Rew}(q,\mathcal{O}),o\in{\sf
prov}_{\mathcal{I}_{\mathcal{D}}}({\boldsymbol{q^{*}}(\vec{a})})\\}.$

[“$\supseteq$”] Let $(q^{*},m^{*})\in\mathsf{Rew}(q,\mathcal{O})$ and let
$o\in{\sf prov}_{\mathcal{I}_{\mathcal{D}}}({\boldsymbol{q^{*}}(\vec{a})})$.

  * •

There is a match $\pi$ of $\boldsymbol{q^{*}}$ to $\mathcal{I}_{\mathcal{D}}$
such that $\pi(\vec{x})=\vec{a}$ and
$o=\prod_{P(\vec{t},t)\in\boldsymbol{q^{*}}}\pi(t)$. Since $\mathcal{D}$ is a
set of annotated assertions, by definition of the canonical model
$\mathcal{I}_{\mathcal{D}}$, it holds that for every
$P(\vec{t},t)\in\boldsymbol{q^{*}}$:

    * –

$(P(\pi(\vec{t})),\pi(t))\in\mathcal{D}$ so
$(P(\pi(\vec{t})),\pi(t))\in\mathsf{saturate}(\mathcal{O})$;

    * –

so $\mathcal{O}\models(P(\pi(\vec{t})),\pi(t))$ by Theorem 4.7;

    * –

so $\mathcal{I}_{\mathcal{O}}\models(P(\pi(\vec{t})),\pi(t))$ by Theorem 3.14.

It follows that $\pi$ is a match of $\boldsymbol{q^{*}}$ to
$\mathcal{I}_{\mathcal{O}}$ such that $\pi(\vec{x})=\vec{a}$ and
$o=\prod_{P(\vec{t},t)\in\boldsymbol{q^{*}}}\pi(t)$.

  * •

Since $(q^{*},m^{*})\in\mathsf{Rew}(q,\mathcal{O})$, there is a rewriting
sequence
$(q_{0},m_{0})\rightarrow_{\mathcal{O}}(q_{1},m_{1})\rightarrow_{\mathcal{O}}\dots\rightarrow_{\mathcal{O}}(q_{k},m_{k})$
such that $(q_{0},m_{0})=(q,1)$ and $(q_{k},m_{k})=(q^{*},m^{*})$. Moreover,
for every $0\leq i\leq k-1$, there is $m_{i,i+1}$ such that
$m_{i+1}=m_{i}\times m_{i,i+1}$.

We show that for every $0\leq j\leq k$ that there is a match $\pi_{j}$ of the
extended version $\boldsymbol{q_{j}}$ of $q_{j}$ to
$\mathcal{I}_{\mathcal{O}}$ such that $\pi_{j}(\vec{x})=\vec{a}$ and
$\prod_{P(\vec{t},t)\in\boldsymbol{q_{j}}}\pi_{j}(t)=\prod_{i=j}^{k-1}m_{i,i+1}\times
o$. The proof is by descending induction on $j$.

_Base case:_ $j=k$, $(q_{k},m_{k})=(q^{*},m^{*})$ and
$\prod_{i=k}^{k-1}m_{i,i+1}\times o=o$. We have shown that there is a match
$\pi$ of $\boldsymbol{q^{*}}$ to $\mathcal{I}_{\mathcal{O}}$ such that
$\pi(\vec{x})=\vec{a}$ and $o=\prod_{P(\vec{t},t)\in\boldsymbol{q^{*}}}\pi(t)$
so we just need to take $\pi_{k}=\pi$.

_Induction step._ Assume that the property is true for some $1\leq j\leq k$:
There is a match $\pi_{j}$ of $\boldsymbol{q_{j}}$ to
$\mathcal{I}_{\mathcal{O}}$ such that $\pi_{j}(\vec{x})=\vec{a}$ and
$\prod_{P(\vec{t},t)\in\boldsymbol{q_{j}}}\pi_{j}(t)=\prod_{i=j}^{k-1}m_{i,i+1}\times
o$.

We show that the property still holds for $j-1$. Since
$(q_{j-1},m_{j-1})\rightarrow_{\mathcal{O}}(q_{j},m_{j})$, there is a variable
$x_{0}$ existentially quantified in $q_{j-1}$ such that no atoms of the form
$R(x_{0},x_{0})$ occur in $q_{j-1}$ and there is $(A\sqsubseteq\exists
P,v)\in\mathcal{O}$ such that $q_{j}$ has been obtained from $q_{j-1}$ by
dropping every atom that contains $x_{0}$, selecting a variable $y_{0}\in
V_{p}$ and replacing every occurrence $y^{\prime}\in V_{p}$ in $q_{j-1}$ by
$y_{0}$ and adding the atoms $\\{D(y_{0})\mid D\in
At(q_{j-1},x_{0},A\sqsubseteq\exists P)\\}$ where:

    * (a)

for every $Q(y,x_{0})\in q_{j-1}$, there exists $(P\sqsubseteq
Q,m_{P\sqsubseteq Q})\in\mathsf{saturate}(\mathcal{O})$, and

    * (b)

for every $C(x_{0})\in q_{j-1}$, there are $p^{C},p^{\prime C}\geq 0$ such
that $(B^{C}_{1}\sqcap\dots\sqcap B^{C}_{p^{C}}\sqcap B^{\prime
C}_{1}\sqcap\dots\sqcap B^{\prime C}_{p^{\prime C}}\sqsubseteq
C,n_{C})\in\mathsf{saturate}(\mathcal{O})$, for every $1\leq i\leq p^{C}$,
there exist $(\exists\mathsf{inv}(P^{C}_{i}).A^{C}_{i}\sqsubseteq
B^{C}_{i},v^{C}_{i})\in\mathcal{O}$ and $(P\sqsubseteq
P^{C}_{i},m^{C}_{i})\in\mathsf{saturate}(\mathcal{O})$, and for every $1\leq
i\leq p^{\prime C}$ there exists $(\top\sqsubseteq
B^{C}_{i},o^{C}_{i})\in\mathsf{saturate}(\mathcal{O})$, and if we let
$m_{C}=\prod_{i=1}^{p^{C}}(v^{C}_{i}\times
m^{C}_{i})\times\prod_{i=1}^{p^{\prime C}}o^{C}_{i}$,

$m_{j-1,j}=mon(q_{j-1},x_{0},A\sqsubseteq\exists
P)=v\times\prod_{Q(y,x_{0})\in q_{j-1}}m_{P\sqsubseteq
Q}\times\prod_{C(x_{0})\in q_{j-1}}m_{C}\times n_{C}.$

First note that since $\pi_{j}$ is a match of $\boldsymbol{q_{j}}$ to
$\mathcal{I}_{\mathcal{O}}$ and for every $D\in
At(q_{j-1},x_{0},A\sqsubseteq\exists P)$,
$D(y_{0},t_{D})\in\boldsymbol{q_{j}}$ (where $t_{D}$ is an existentially
quantified variable that does not occur anywhere else), it holds that
$\mathcal{I}_{\mathcal{O}}\models(D(\pi_{j}(y_{0})),\pi_{j}(t_{D}))$ for every
$D\in At(q_{j-1},x_{0},A\sqsubseteq\exists P)$. Since $A\in
At(q_{j-1},x_{0},A\sqsubseteq\exists P)$ and $(A\sqsubseteq\exists
P,v)\in\mathcal{O}$ it follows that there exists
$e\in\Delta^{\mathcal{I}_{\mathcal{O}}}$ such that
$(\pi_{j}(y_{0}),e,\pi_{j}(t_{A})\times v)\in P^{\mathcal{I}_{\mathcal{O}}}$.

Let $P(\vec{t},t)\in\boldsymbol{q_{j-1}}$.

    * –

If $P(\vec{t},t)\in\boldsymbol{q_{j}}$, $\pi_{j}(\vec{t},t)\in
P^{\mathcal{I}_{\mathcal{O}}}$ by definition of $\pi_{j}$.

    * –

Otherwise, if $P(\vec{t},t)\notin\boldsymbol{q_{j}}$, either
$P(\vec{t},t)=Q(y,x_{0},t)$ for some $Q\in{\sf N_{R}}$ and $y\in V_{p}$, or
$P(\vec{t},t)=C(x_{0},t)$ for some $C\in{\sf N_{C}}$.

      * *

In the first case, $Q(y,x_{0})\in q_{j-1}$ so there is $(P\sqsubseteq
Q,m_{P\sqsubseteq Q})\in\mathsf{saturate}(\mathcal{O})$.

By Lemma B.8, $\mathcal{O}\models(P\sqsubseteq Q,m_{P\sqsubseteq Q})$ so
$\mathcal{I}_{\mathcal{O}}\models(P\sqsubseteq Q,m_{P\sqsubseteq Q})$.

Hence, since $(\pi_{j}(y_{0}),e,\pi_{j}(t_{A})\times v)\in
P^{\mathcal{I}_{\mathcal{O}}}$, it holds that
$(\pi_{j}(y_{0}),e,\pi_{j}(t_{A})\times v\times m_{P\sqsubseteq Q})\in
Q^{\mathcal{I}_{\mathcal{O}}}$.

      * *

In the second case, $C(x_{0})\in q_{j-1}$ so there are $p^{C},p^{\prime C}\geq
0$ such that $(B^{C}_{1}\sqcap\dots\sqcap B^{C}_{p^{C}}\sqcap B^{\prime
C}_{1}\sqcap\dots\sqcap B^{\prime C}_{p^{\prime C}}\sqsubseteq
C,n_{C})\in\mathsf{saturate}(\mathcal{O})$, for every $1\leq i\leq p^{C}$,
there exist $(\exists\mathsf{inv}(P^{C}_{i}).A^{C}_{i}\sqsubseteq
B^{C}_{i},v^{C}_{i})\in\mathcal{O}$ and $(P\sqsubseteq
P^{C}_{i},m^{C}_{i})\in\mathsf{saturate}(\mathcal{O})$, and for every $1\leq
i\leq p^{\prime C}$ there exists $(\top\sqsubseteq
B^{C}_{i},o^{C}_{i})\in\mathsf{saturate}(\mathcal{O})$.

As above, by Lemma B.8, and the fact that
$\mathcal{I}_{\mathcal{O}}\models\mathcal{O}$, we obtain that
$\mathcal{I}_{\mathcal{O}}\models(B^{C}_{1}\sqcap\dots\sqcap
B^{C}_{p^{C}}\sqcap B^{\prime C}_{1}\sqcap\dots\sqcap B^{\prime C}_{p^{\prime
C}}\sqsubseteq C,n_{C})$, for $1\leq i\leq p^{C}$,
$\mathcal{I}_{\mathcal{O}}\models(\exists\mathsf{inv}(P^{C}_{i}).A^{C}_{i}\sqsubseteq
B^{C}_{i},v^{C}_{i})$ and $\mathcal{I}_{\mathcal{O}}\models(P\sqsubseteq
P^{C}_{i},m^{C}_{i})$, and for every $1\leq i\leq p^{\prime C}$,
$\mathcal{I}_{\mathcal{O}}\models(\top\sqsubseteq B^{C}_{i},o^{C}_{i})$.

It follows that:

        * ·

For $1\leq i\leq p^{C}$, $(\pi_{j}(y_{0}),e,\pi_{j}(t_{A})\times v\times