$h(x_{i})=(c_{a,i,r,A},c_{b,i,r,B})$ for $i\in\\{1,\ldots,4\\}$. Since only
the cycle consisting of not unraveled individuals remains, the Unravel step
cannot be applied.

To deal with this issue, we apply the original $\mathsf{refine}$ subroutine
from Section 3.3 to $\mathcal{B}_{n}$ (with $n_{\text{max}}=3$), resulting in
a sequence
$(\mathcal{B}_{n},\bar{b}_{n}),(\mathcal{B}_{n+1},\bar{b}_{n+1}),\dots$ where
$\bar{b}_{n}=a_{1}\otimes a_{2}$, in a slightly adapted way:

  1. 1.

the individuals in $I$ are not touched, that is, no cycle that involves an
individual from $I$ is considered in the Expansion step nor is any assertion
removed during the Minimize step that contains an individual from $I$;

  2. 2.

as a consequence, the Expansion step cannot involve individuals in
$\bar{a}_{1}\otimes\bar{a}_{2}$, and thus the exponential blowup in the arity
is avoided. In fact, $\bar{b}_{n}=\bar{b}_{n+1}=\cdots$.

  3. 3.

the Splitting step is not applied.

We now analyze the second version of $\mathsf{refine}$, starting with the
following lemma.

######  Lemma 20.

Let $i\geq 1$. Every cycle in $\mathcal{B}_{i}$ of length at most three
consists only of individuals from
$\mathsf{ind}(\mathcal{A}_{1})\times\mathsf{ind}(\mathcal{A}_{2})$.

###### Proof.

We prove the lemma by induction on $i$. In the induction start,
$\mathcal{B}_{1}=\mathsf{minimize}(\mathcal{C}^{3}_{\mathcal{A}_{1},\mathcal{O}}\times\mathcal{C}^{3}_{\mathcal{A}_{2},\mathcal{O}})$.
If $\mathcal{B}_{1}$ contains a cycle $r((a_{1},a_{2}),(a_{1},a_{2}))$ of
length 1 with $a_{i}\notin\mathcal{A}_{i}$ for some $i\in\\{1,2\\}$, then
$r(a_{1},a_{1})$ is a cycle of length 1 in
$\mathcal{C}^{3}_{\mathcal{A}_{1},\mathcal{O}}$ which is not the case by Lemma
2. Next assume that $\mathcal{B}_{1}$ contains a cycle
$r_{0}((a_{1},a_{2}),(b_{1},b_{2})),r_{1}((b_{1},b_{2}),(a_{1},a_{2}))$ of
length 2. Assume w.l.o.g. that $a_{1}\notin\mathsf{ind}(\mathcal{A}_{1})$. If
$a_{1}=b_{1}$, then $r_{0}(a_{1},a_{1})$ is a cycle of length 1 in
$\mathcal{C}^{3}_{\mathcal{A}_{1},\mathcal{O}}$, but this is not the case by
Lemma 2. If $a_{1}\neq b_{1}$, then $r_{0}(a_{1},b_{1}),r_{1}(b_{1},a_{1})$ is
a cycle of length 2 in $\mathcal{C}^{3}_{\mathcal{A}_{1},\mathcal{O}}$, which
again contradicts Lemma 2. If $\mathcal{B}_{1}$ contains a cycle
$r_{0}((a_{1},a_{2}),(b_{1},b_{2}))$, $r_{1}((b_{1},b_{2}),(c_{1},c_{2}))$,
$r_{2}((c_{1},c_{2}),(a_{1},a_{2}))$ of length 3, we can argue similarly that
$\mathcal{C}^{3}_{\mathcal{A}_{1},\mathcal{O}}$ contains a cycle of length 1
or 3 that involves an individual not in $\mathsf{ind}(\mathcal{A}_{i})$, again
obtaining a contradiction.

For the induction step, we show that both the Minimize step and the Unravel
step do not create cycles of length 1, 2, or 3 that involve individuals not
from $\mathsf{ind}(\mathcal{A}_{1})\times\mathsf{ind}(\mathcal{A}_{2})$. Since
the Minimize step only removes assertions, it cannot create any new cycles.
For the Unravel step, let the lemma hold for $\mathcal{B}_{i}$ and let
$\mathcal{B}$ be $\mathcal{B}_{i}$ after the Unravel step. Let
$r_{0}((a_{1},a_{2}),(b_{1},b_{2}))$, $r_{1}((b_{1},b_{2}),(c_{1},c_{2}))$,
$r_{2}((c_{1},c_{2}),(a_{1},a_{2}))$ be a new cycle of length $3$ in
$\mathcal{B}$. Since the cycle is new, one of $(a_{1},a_{2})$, $(b_{1},b_{2})$
or $(c_{1},c_{2})$ must be $(d_{1}^{\prime},d_{2}^{\prime})$, a new individual
created by the Unravel. But by the definition of the Unravel step, replacing
$(d_{1}^{\prime},d_{2}^{\prime})$ with $(d_{1},d_{2})$ in the cycle must yield
a cycle in $\mathcal{B}_{i}$ which contradicts the induction hypothesis. The
same argument can be applied to cycles of length 1 and 2. ∎

Recall that we first construct a sequence
$\mathcal{B}_{1},\mathcal{B}_{2},\dots$ using the Unravel and Minimize steps.
With $\mathcal{B}_{i}^{\prime}$, $i\geq 1$, we denote the result of only
applying the Unravel step to $\mathcal{B}_{i}$, but not the Minimize step.

######  Lemma 21.

For all $i\geq 1$, $\mathcal{B}_{i}^{\prime},a\preceq\mathcal{B}_{i},a$ and
$\mathcal{B}_{i},a\preceq\mathcal{B}_{i}^{\prime},a$, for all
$a\in\mathsf{ind}(\mathcal{B}_{i})\cap\mathsf{ind}(\mathcal{B}_{i}^{\prime})$,
and $\mathcal{B}_{i}^{\prime},a^{\prime}\preceq\mathcal{B}_{i},a$ and
$\mathcal{B}_{i},a\preceq\mathcal{B}_{i}^{\prime},a^{\prime}$ for all copies
$a^{\prime}\in\mathsf{ind}(\mathcal{B}_{i}^{\prime})\setminus\mathsf{ind}(\mathcal{B}_{i})$
of some $a\in\mathsf{ind}(\mathcal{B}_{i})$.

###### Proof.

Define a relation
$S\subseteq\mathsf{ind}(\mathcal{B}_{i})\times\mathsf{ind}(\mathcal{B}_{i}^{\prime})$
by taking:

  * •

$(a,a)\in S$, for all
$a\in\mathsf{ind}(\mathcal{B}_{i})\cap\mathsf{ind}(\mathcal{B}_{i}^{\prime})$,
and

  * •

$(a,a^{\prime})\in S$, for all copies
$a^{\prime}\in\mathsf{ind}(\mathcal{B}_{i}^{\prime})$ of some element
$a\in\mathsf{ind}(\mathcal{B}_{i})$.

It is routine to verify that $S$ serves as witness for the claimed simulations
from $\mathcal{B}_{i}$ to $\mathcal{B}_{i}^{\prime}$, and its inverse $S^{-}$
serves as witness for the claimed simulations from $\mathcal{B}_{i}^{\prime}$
to $\mathcal{B}_{i}$. ∎

The next lemma is the most intricate to prove in the analysis of the second
version of $\mathsf{refine}$.

######  Lemma 22.

For all $i\geq 1$, $\mathcal{B}_{i},\mathcal{O}\models
q_{T}(\bar{a}_{1}\otimes\bar{a}_{2})$.

###### Proof.

We prove the lemma by induction on $i$. The induction start is immediate since
$\mathcal{U}_{\mathcal{A}_{1},\mathcal{O}}\times\mathcal{U}_{\mathcal{A}_{2},\mathcal{O}}\models
q_{T}(\bar{a}_{1}\otimes\bar{a}_{2})$ and there is a homomorphism from
$\mathcal{U}_{\mathcal{A}_{1},\mathcal{O}}\times\mathcal{U}_{\mathcal{A}_{2},\mathcal{O}}$
to
$\mathcal{C}^{3}_{\mathcal{A}_{1},\mathcal{O}}\times\mathcal{C}^{3}_{\mathcal{A}_{2},\mathcal{O}}$
that is the identity on $\bar{a}_{1}\otimes\bar{a}_{2}$. Thus,
$\mathcal{C}^{3}_{\mathcal{A}_{1},\mathcal{O}}\times\mathcal{C}^{3}_{\mathcal{A}_{2},\mathcal{O}},\mathcal{O}\models
q_{T}(\bar{a}_{1}\otimes\bar{a}_{2})$. It remains to note that
$\mathcal{B}_{1}=\mathsf{minimize}(\mathcal{C}^{3}_{\mathcal{A}_{1},\mathcal{O}}\times\mathcal{C}^{3}_{\mathcal{A}_{2},\mathcal{O}})$
and that the Minimize step preserves $\mathcal{B}_{1},\mathcal{O}\models
q_{T}(\bar{a}_{1}\otimes\bar{a}_{2})$.

For the induction step, consider $\mathcal{B}_{i+1}$ with $i\geq 1$. By
induction hypothesis, there is a homomorphism $h$ from $q_{T}$ to
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ with
$h(\bar{x})=\bar{a}_{1}\otimes\bar{a}_{2}$. By Lemma 9, we can assume that
$q_{T}$ is strongly symmetry-free. Let $\mathcal{B}$ be the result of applying
the unraveling step to $\mathcal{B}_{i}$, and let $U$ be the set of all
individuals $(d_{1},d_{2})\in\mathsf{Ind}(\mathcal{B}_{i})$ such that some
assertion $r((c_{1},c_{2}),(d_{1},d_{2}))$ was removed in that step. Note that
if $(d_{1},d_{2})\in U$, then
$(d_{1},d_{2})\notin\mathsf{Ind}(\mathcal{A}_{1})\times\mathsf{Ind}(\mathcal{A}_{2})$.
In what follows, we construct a homomorphism $g$ from $q_{T}$ to
$\mathcal{U}_{\mathcal{B},\mathcal{O}}$ with
$g(\bar{x})=\bar{a}_{1}\otimes\bar{a}_{2}$. Thus,
$\mathcal{B},\mathcal{O}\models q_{T}(\bar{a}_{1}\otimes\bar{a}_{2})$. By
definition of the Minimize step, this implies
$\mathcal{B}_{i+1},\mathcal{O}\models q_{T}(\bar{a}_{1}\otimes\bar{a}_{2})$ as
desired.

We first observe the following, which can be proved by a straightforward
induction on $j$.

Claim 1. For all $j\geq 0$, if
$R((c_{1},c_{2}),(d_{1},d_{2}))\in\mathcal{B}_{j}$ with $(c_{1},c_{2})$
unraveled and $(d_{1},d_{2})$ not unraveled, then $R$ is a role name, but not
an inverse role.

For a variable $x$ in $q_{T}$, let us denote with $V_{x}$ the set of all atoms
$R(x,y)\in q_{T}$ such that $h(y)\in\mathsf{Ind}(\mathcal{B}_{i})$ is
unraveled. We observe the following.

Claim 2. Let $x\in\mathsf{var}(q_{T})$ such that $h(x)=(d_{1},d_{2})\in U$.
Then there is a role name $r$ such that all atoms in $V_{x}$ are of shape
$r(y,x)$ and one of the following is the case:

  1. (i)

$V_{x}$ is a singleton;

  2. (ii)

$d_{1}$ has the form $c_{b,0,r,C}$ and for every $r(y,x)\in V_{x}$,
$\mathcal{A}_{2}$ contains an assertion $r(b^{\prime},d_{2})$ with
$h(y)=(b,b^{\prime})$;

  3. (iii)

$d_{2}$ has the form $c_{b,0,r,C}$ and for every $r(y,x)\in V_{x}$,
$\mathcal{A}_{1}$ contains an assertion $r(b^{\prime},d_{1})$ with
$h(y)=(b^{\prime},b)$;

  4. (iv)

$d_{1}$ has the form $c_{b_{1},0,r,C_{1}}$, $d_{2}$ has the form
$c_{b_{2},0,r,C_{2}}$, and $h(y)=(b_{1},b_{2})$ for every $r(y,x)\in V_{x}$.

Proof of Claim 2. To show the first part, let $R(y_{1},x),S(y_{2},x)\in
V_{x}$. Since $h(x)=(d_{1},d_{2})$ is not unraveled, but $h(y_{1})$ and
$h(y_{2})$ are unraveled, $R$ and $S$ are role names by Claim 1. Moreover,
$(d_{1},d_{2})$ not being unraveled means that at least one one of the $d_{j}$
takes the shape $c_{a,k,r,C}$ for some role name $r$. By definition of
$\mathcal{C}^{3}_{\mathcal{A}_{j},\mathcal{O}}$, for every
$s(d,c_{a,k,r,C})\in\mathcal{C}^{3}_{\mathcal{A}_{j},\mathcal{O}}$, we have
$s=r$. Hence, for every $s(d,(d_{1},d_{2}))\in\mathcal{B}_{i}$ we have $s=r$
as well. Thus, $R=S=r$ and all assertions in $V_{x}$ are based on the same
role name $r$.

Now for the second part. Assume that Case (i) does not apply. Then we find
$r(y_{1},x),r(y_{2},x)\in V_{x}$ with $y_{1}\neq y_{2}$. Since $q_{T}$ is
strongly symmetry-free and $x$ is not an answer variable (which follows from
$h(x)\in U$) one of the atoms, say $r(y_{1},x)$, occurs on a cycle $p$ in
$q_{T}$. Since $q_{T}$ is chordal, we can assume that $p$ has length at most
three. Since $h$ is a homomorphism from $q_{T}$ to
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$, the ‘$h$-image of $p$’ contains a
cycle $p^{\prime}$ of length at most three in $\mathcal{B}_{i}$. By Lemma 20,
$p^{\prime}$ consists only of elements from
$\mathsf{ind}(\mathcal{A}_{1})\times\mathsf{ind}(\mathcal{A}_{2})$. Thus
$h(x)$ cannot be involved in $p^{\prime}$, since $h(x)=(d_{1},d_{2})$ is not
unraveled. Consequently, the cycle $p$ has to be of the shape

$r(y_{1},x),r^{-}(x,z),s(y_{1},z)$

and
$h(y_{1})=h(z)=(b_{1},b_{2})\in\mathsf{ind}(\mathcal{A}_{1})\times\mathsf{ind}(\mathcal{A}_{2})$.
It follows that we must have $i=1$ since for $i>1$, all successors of elements
of $\mathsf{ind}(\mathcal{A}_{1})\times\mathsf{ind}(\mathcal{A}_{2})$ are
unraveled. We distinguish the following cases:

  * •

$d_{1}\in\mathsf{ind}(\mathcal{A}_{1})$ and
$d_{2}\in\mathsf{ind}(\mathcal{A}_{2})$.

Impossible because $(d_{1},d_{2})$ is not unraveled.

  * •

$d_{1}$ has shape $c_{b_{1},0,r,C_{1}}$ and $d_{2}$ has shape
$c_{b_{2},0,r,C_{2}}$. By definition of the models
$\mathcal{C}_{\mathcal{A}_{i},\mathcal{O}}^{3}$ and since in
$\mathcal{B}_{1}\subseteq\mathcal{C}^{3}_{\mathcal{A}_{1},\mathcal{O}}\times\mathcal{C}^{3}_{\mathcal{A}_{2},\mathcal{O}}$,
$(b_{1},b_{2})$ is the unique unraveled $r$-predecessor of $(d_{1},d_{2})$ in
$\mathcal{B}_{i}=\mathcal{B}_{1}$. Then we are in Case (iv).

  * •

$d_{1}$ has shape $c_{b_{1},0,r,C}$ and
$d_{2}\in\mathsf{ind}(\mathcal{A}_{2})$.

Then $b_{1}$ is the unique $r$-predecessor of $d_{1}$ in
$\mathcal{C}^{3}_{\mathcal{A}_{1},\mathcal{O}}$ that can appear in the first
component of an unraveled element. Let $r(y,x)\in V_{x}$. Because $h(y)$ is
unraveled and $i=1$,
$h(y)\in\mathsf{ind}(\mathcal{A}_{1})\times\mathsf{ind}(\mathcal{A}_{2})$.
Since
$\mathcal{B}_{1}\subseteq\mathcal{C}^{3}_{\mathcal{A}_{1},\mathcal{O}}\times\mathcal{C}^{3}_{\mathcal{A}_{2},\mathcal{O}}$,
$r(y,x)\in V_{x}$ thus implies that there is an assertion
$r(b^{\prime},d_{2})\in\mathcal{A}_{2}$ such that $h(y)=(b_{1},b^{\prime})$.
Thus, we are in Case (ii).

  * •

$d_{2}$ has shape $c_{b_{2},0,r,C}$ and
$d_{1}\in\mathsf{ind}(\mathcal{A}_{1})$.

We argue as in the previous case, but end up in Case (iii).

This finishes the proof of Claim 2. For the next claim, we associate with
every variable $x\in\mathsf{var}(q_{T})$ with
$h(x)\in\mathsf{ind}(\mathcal{B}_{i})$ the set $Z_{x}$ that consists of all
variables $y\in\mathsf{var}(q_{T})$ such that $q_{T}$ contains a path
$R_{0}(z_{0},z_{1}),\ldots,R_{m-1}(z_{m-1},z_{m})$ from $x$ to $y$ where
$h(z_{1}),\dots,h(z_{m})$ are all located in the subtree of
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ rooted at $h(x)$, but are
different from $h(x)$.

Claim 3. For all $y\in\mathsf{var}(q_{T})$ with
$h(y)\notin\mathsf{ind}(\mathcal{B}_{i})$, there is at most one
$x\in\mathsf{var}(q_{T})$ with $y\in Z_{x}$ and $h(x)\in U$.

Proof of Claim 3. Suppose that $y\in\mathsf{var}(q_{T})$ with
$h(y)\notin\mathsf{ind}(\mathcal{B}_{i})$ and that there are distinct
variables $x_{1},x_{2}\in\mathsf{var}(q_{T})$ with $y\in Z_{x_{j}}$ and
$h(x_{j})\in U$ for $j\in\\{1,2\\}$. Let

$\displaystyle
p_{1}=R_{0}(z_{0},z_{1}),\ldots,R_{n}(z_{n-1},z_{n})\quad\text{and}\quad$
$\displaystyle
p_{2}=S_{0}(z_{0}^{\prime},z_{1}^{\prime}),\ldots,S_{m}(z_{m-1}^{\prime},z_{m}^{\prime})$

be paths in $q_{T}$ from $x_{1}$ to $y$ and from $x_{2}$ to $y$, respectively,
such that $h(z_{j})\neq h(x_{1})$ for all $j\in\\{1,\ldots,n\\}$ and
$h(z_{j}^{\prime})\neq h(x_{2})$ for all $j\in\\{1,\ldots,m\\}$. Note that $h$
is a homomorphism from $p_{j}$ to the subtree of
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ rooted at $h(x_{j})$, for
$j\in\\{1,2\\}$. Since $h(y)$ is both in the subtree below $h(x_{1})$ and
below $h(x_{2})$, we have $h(x_{1})=h(x_{2})$.

We analyze the structure of the paths $p_{1}$ and $p_{2}$. Let us first verify
that all $R_{j}$ and all $S_{j}$ can be assumed to be role names. We do this
explicitly only for the $R_{j}$. Let $\mathbf{S}$ denote the subtree of
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ rooted at $h(x_{1})$, that is, the
restriction of $\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ to all traces that
start with $h(x_{1})$, including $h(x_{1})$ itself. By construction of
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$, $\mathbf{S}$ is a ditree. Then
$R_{0}$ must be a role name since $R_{0}(h(x_{1}),h(z_{1}))\in\mathbf{S}$,
$h(x_{1})$ is the root of $\mathbf{S}$, and $h(z_{1})$ in $\mathbf{S}$. Now,
let $\ell$ be minimal such that $R_{\ell}$ is an inverse role $r^{-}$ and
consider the atoms
$R_{\ell-1}(z_{\ell-1},z_{\ell}),r^{-}(z_{\ell},z_{\ell+1})$ in $q_{T}$. Since
$h$ is a homomorphism and $\mathbf{S}$ is a ditree, we know that
$R_{\ell-1}=r$, and thus there are atoms
$r(z_{\ell-1},z_{\ell}),r(z_{\ell+1},z_{\ell})$ in $q_{T}$.

Now, if $z_{\ell-1}=z_{\ell+1}$, we can drop these two atoms from the path.
Otherwise, since $q_{T}$ is strongly symmetry-free and $z_{\ell}$ is not an
answer variable (as $h(z_{\ell})$ is in $\mathbf{S}$ but different from its
root), one of these atoms occurs on a cycle $p$ in $q_{T}$. Let us assume that
this is atom $r(z_{\ell-1},z_{\ell})$, the case of atom
$r(z_{\ell+1},z_{\ell})$ is analogous. Since $q_{T}$ is chordal, we can assume
that $p$ has length at most three. Since $h$ is a homomorphism from $q_{T}$ to
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$, the image of $p$ contains a cycle
$p^{\prime}$ of length at most three in
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$. Even if $h$ is not injective, the
cycle $p^{\prime}$ must contain $h(z_{\ell})$ or $h(z_{\ell-1})$. However,
both possibilities lead to a contradiction. If $p^{\prime}$ contains
$h(z_{\ell})$, then
$h(z_{\ell})\in\mathsf{ind}(\mathcal{A}_{1})\times\mathsf{ind}(\mathcal{A}_{2})$
by Lemma 20 but this is not the case since $h(z_{\ell})$ is in $\mathbf{S}$
and different from $h(x_{1})$. If $p^{\prime}$ contains $h(z_{\ell-1})$, then
$h(z_{\ell-1})$ must be $h(x_{1})$, and $p^{\prime}$ witnesses that
$h(x_{1})\in\mathsf{ind}(\mathcal{A}_{1})\times\mathsf{ind}(\mathcal{A}_{2})$,
in contradiction to $h(x_{1})\in U$.

At this point, we have established that all $R_{j}$ and $S_{j}$ are role names
$r_{j},s_{j}$. Since $\mathbf{S}$ is a ditree, it follows that $m=n$ and
$r_{j}=s_{j}$ for all $j$. Since $z_{0}\neq z_{0}^{\prime}$ and
$z_{n}=z_{m}^{\prime}$, there is some $\ell>0$ such that
$z_{\ell}=z^{\prime}_{\ell}$, $z_{\ell-1}\neq z^{\prime}_{\ell-1}$. But then
$q_{T}$ contains atoms
$r_{\ell}(z_{\ell-1},z_{\ell}),r_{\ell}(z_{\ell-1}^{\prime},z_{\ell})$. This
leads to a contradiction in the same way as above. This finishes the proof of
Claim 3.

We now define the required homomorphism $g$ in four stages, as follows.

  1. 1.

Define $g(x)=h(x)$ for all $x\in\mathsf{var}(q_{T})$ such that
$h(x)\in\mathsf{ind}(\mathcal{B}_{i})\setminus U$ or $h(x)$ is in the subtree
below some element $d\notin U$.

  2. 2.

For every $x\in\mathsf{var}(q_{T})$ with $h(x)=(d_{1},d_{2})\in U$, we
distinguish cases according to Claim 2:

    1. (a)

If $V_{x}=\emptyset$, then define $g(x)=h(x)$. We argue that this is well-
defined, that is, $h(x)\in\mathsf{ind}(\mathcal{B})$. Suppose to the contrary
that $h(x)\notin\mathsf{ind}(\mathcal{B})$. By definition of the unraveling
operation, this can only be the case if $\mathcal{B}_{i}$ contains only a
single assertion that mentions $h(x)$ and this assertion is of shape
$r((c_{1},c_{2}),h(x))$ with $(c_{1},c_{2})$ unraveled. Since $x$ has to occur
in some atom in $q_{T}$ and $h$ is a homomorphism, $x$ occurs in an atom
$r(z,x)\in q_{T}$ such that $h(z)=(c_{1},c_{2})$. Hence, $r(z,x)\in
V_{x}\neq\emptyset$, contradiction.

    2. (b)

If Case (i) applies and $V_{x}=\\{r(y,x)\\}$, define $g(x)$ to be the copy
$(d_{1}^{\prime},d_{2}^{\prime})$ of $(d_{1},d_{2})$ introduced when
unraveling $r(h(y),h(x))\in\mathcal{B}_{i}$.

    3. (c)

If $V_{x}\neq\emptyset$ and Case (ii) applies (but Case (i) does not), then
define $g(x)$ to be the copy $(brC,d_{2})$ of $(d_{1},d_{2})$, where $b,C$ are
as in Case (ii) of Claim 2.

    4. (d)

If $V_{x}\neq\emptyset$ and Case (iii) applies (but Case (i) does not),
analogously define $g(x)$ to be the copy $(d_{1},brC)$.

    5. (e)

If $V_{x}\neq\emptyset$ and Case (iv) applies (but Case (i) does not), define
$g(x)$ to be the copy $(b_{1}rC_{1},b_{2}rC_{2})$ where
$b_{1},b_{2},C_{1},C_{2}$ are as in Case (iv).

  3. 3.

For every $x$ with $h(x)\in U$ and every $y\in Z_{x}$, $h(y)$ is a trace that
starts with $h(x)$, c.f. the definition of
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$. Define $g(y)$ to be the same
trace, but with the first element $h(x)$ replaced by $g(x)$. It can be
verified that $g(y)$ is indeed an element in
$\mathcal{U}_{\mathcal{B},\mathcal{O}}$ using the fact that, by Lemma 21, the
subtrees below $g(x)$ and $h(x)$ in $\mathcal{U}_{\mathcal{B},\mathcal{O}}$
and $\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$, respectively, are identical.

  4. 4.

For every $y$ with $h(y)$ in the subtree below some $(d_{1},d_{2})\in U$ but
different from $(d_{1},d_{2})$, and such that $y\notin Z_{x}$ for all $x$ with
$h(x)\in U$, choose some copy $(d^{\prime}_{1},d^{\prime}_{2})$ of
$(d_{1},d_{2})$ and define $g(x)$ to be the trace $h(x)$ with the first
element $(d_{1},d_{2})$ replaced by $(d^{\prime}_{1},d^{\prime}_{2})$.

It is easy to see that the four stages above define $g(x)$ for all
$x\in\mathsf{var}(q_{T})$.

Claim 4. $g$ is a homomorphism from $q_{T}$ to
$\mathcal{U}_{\mathcal{B},\mathcal{O}}$ with
$g(\bar{x})=\bar{a}_{1}\otimes\bar{a}_{2}$.

Proof of Claim 4. For $g(\bar{x})=\bar{a}_{1}\otimes\bar{a}_{2}$, observe that
$h(x)\in\mathsf{ind}(\mathcal{A}_{1})\times\mathsf{ind}(\mathcal{A}_{2})$ for
every $x\in\bar{x}$ while
$U\cap(\mathsf{ind}(\mathcal{A}_{1})\times\mathsf{ind}(\mathcal{A}_{2}))=\emptyset$.
Thus, Stage 1 of the definition of $g$ implies $g(\bar{x})=h(\bar{x})$.

Now, let $A(x)\in q_{T}$ and thus
$A(h(x))\in\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$. We distinguish the
following cases:

  * •

If $g(x)$ was defined in Stage 1, then $g(x)=h(x)$. First assume that
$g(x)\in\mathsf{Ind}(\mathcal{B}_{i})$. By Lemma 21, we have
$\mathcal{B}_{i},h(x)\preceq\mathcal{B},g(x)$ and thus, by Lemma 7 Point 2
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}},h(x)\preceq\mathcal{U}_{\mathcal{B},\mathcal{O}},g(x)$.
Hence, also $A(g(x))\in\mathcal{U}_{\mathcal{B},\mathcal{O}}$ by Lemma 6. Now
assume that $g(x)\notin\mathsf{Ind}(\mathcal{B}_{i})$. Then $h(x)=g(x)$ is a
trace and traces in $\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ and
$\mathcal{U}_{\mathcal{B},\mathcal{O}}$ that end with the same concept $C$
must satisfy the same concept names.

  * •

If $g(x)$ was defined in Stage 2, then $g(x)=(d_{1}^{\prime},d_{2}^{\prime})$
is a copy of $h(x)=(d_{1},d_{2})$ or $g(x)=h(x)$. By Lemma 21, we have
$\mathcal{B}_{i},h(x)\preceq\mathcal{B},g(x)$, thus
$A(g(x))\in\mathcal{U}_{\mathcal{B},\mathcal{O}}$ by Lemmas 6 and 7.

  * •

If $g(x)$ was defined in Stage 3 or 4, then $h(x)$ and $g(x)$ are both traces
that end with the same concept $C$ and, by construction of universal models,
thus make true the same concept names. Consequently,
$A(h(x))\in\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ implies
$A(g(x))\in\mathcal{U}_{\mathcal{B},\mathcal{O}}$.

Finally, let $r(x,y)\in q_{T}$ and thus
$r(h(x),h(y))\in\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$. We distinguish the
following cases:

  * •

It cannot be that both $h(x)$ and $h(y)$ are elements of $U$, by definition of
the unraveling step.

  * •

If both $h(x)$ and $h(y)$ are not elements of $U$, then both $g(x)$ and $g(y)$
were defined in the same stage, one of Stage 1, 3, and 4. We can then argue
very similar to the case of concept atoms that
$r(g(x),g(y))\in\mathcal{U}_{\mathcal{B},\mathcal{O}}$.

  * •

If $h(x)=(d_{1},d_{2})\in U$ and $h(y)\notin U$, then we distinguish cases:

    * –

If $h(y)\notin\mathsf{ind}(\mathcal{B}_{i})$, then it is an $r$-successor of
$(d_{1},d_{2})$ in the tree below $(d_{1},d_{2})$ in
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$. Thus $g(y)$ was defined in Stage
3. If $h(y)$ is trace $(d_{1},d_{2})rC$, then $g(y)$ is trace
$(d^{\prime}_{1},d^{\prime}_{2})rC$ for
$g(x)=(d^{\prime}_{1},d^{\prime}_{2})$. It follows that
$r(g(x),g(y))\in\mathcal{U}_{\mathcal{B},\mathcal{O}}$.

    * –

If $h(y)\in\mathsf{ind}(\mathcal{B}_{i})$ is not unraveled, then by definition
of the unraveling step, we have
$r((d_{1}^{\prime},d_{2}^{\prime}),h(y))\in\mathcal{B}$ for all copies
$(d^{\prime}_{1},d_{2}^{\prime})$ of $(d_{1},d_{2})$, and
$r((d_{1},d_{2}),h(y))\in\mathcal{B}$. We know that $g(x)$ was defined in
Stage 2 and is either $h(x)$ or some copy thereof, and $h(y)$ was defined in
Stage 1, thus $g(y)=h(y)$. Consequently,
$r(g(x),g(y))\in\mathcal{B}\subseteq\mathcal{U}_{\mathcal{B},\mathcal{O}}$.

    * –

It cannot be the case that $h(y)\in\mathsf{ind}(\mathcal{B}_{i})$ is
unraveled: By Claim 2, $S$ is a role name for every atom $S(z,x)\in q_{T}$
such that $h(z)$ is unraveled. However, this is not the case for the atom
$r^{-}(y,x)\in q_{T}$ we started with.

  * •

If $h(x)\notin U$ and $h(y)=(d_{1},d_{2})\in U$, then
$h(x)\in\mathsf{ind}(\mathcal{B}_{i})$ since
$r(h(x),h(y))\in\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ and by definition
of universal models. We distinguish cases according to Claim 2:

    * –

If $V_{y}=\emptyset$, then $g(y)=h(y)$, by Stage 2(a). Moreover, as
$h(x)\in\mathsf{ind}(\mathcal{B}_{i})\setminus U$, we have $g(x)=h(x)$, by
Stage 1. Hence,
$r(g(x),g(y))\in\mathcal{B}\subseteq\mathcal{U}_{\mathcal{B},\mathcal{O}}$.

    * –

If Case (i) applies and $V_{y}=\\{r(x,y)\\}$ with $h(x)$ unraveled, then
$g(y)$ was defined in Stage 2(b) and
$r(g(x),g(y))\in\mathcal{U}_{\mathcal{B},\mathcal{O}}$.

    * –

If Case (ii) applies to $V_{y}$, then $d_{1}$ has the form $c_{b,0,r,C}$ and
for every $r(z,y)\in V_{y}$, $\mathcal{A}_{2}$ contains an assertion
$r(b^{\prime},d_{2})$ with $h(z)=(b,b^{\prime})$. Moreover, $g(y)$ was defined
in Stage 2(c) and $g(y)=(brC,d_{2})$.

      * *

If $h(x)$ is unraveled, then $h(x)=g(x)=(b,b^{\prime})$. By definition of the
unraveling, $r((b,b^{\prime}),(brC,d_{2})\in\mathcal{B}$. Hence,
$r(g(x),g(y))\in\mathcal{B}\subseteq\mathcal{U}_{\mathcal{B},\mathcal{O}}$.

      * *

If $h(x)$ is not unraveled, then it was defined in Stage 1 and $h(x)=g(x)$. By
definition of the unraveling, $r(h(x),(brC,d_{2}))\in\mathcal{B}$.

    * –

If Case (iii) applies to $V_{y}$, the argument is symmetric.

    * –

If Case (iv) applies to $V_{y}$, then $d_{1}$ has the form
$c_{b_{1},0,r,C_{1}}$, $d_{2}$ has the form $c_{b_{2},0,r,C_{2}}$,
$h(x)=(b_{1},b_{2})$, and $g(y)$ was defined in Stage 2(e) and
$g(y)=(b_{1}rC_{1},b_{2}rC_{2})$. Since $h(x)$ is unraveled, we have
$g(x)=h(x)$ by Stage 1, and the definition of the unraveling yields
$r(g(x),g(y))\in\mathcal{B}$.

This finishes the proof of Claim 4 and thus of the lemma. ∎

######  Lemma 23.

For all $i\geq 1$,

  1. 1.

$\mathcal{B}_{i}$ is $\mathcal{O}$-saturated;

  2. 2.

If $h$ is a homomorphism from $q_{T}$ to
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ with
$h(\bar{y})=\bar{a}_{1}\otimes\bar{a}_{2}$, then
$\mathsf{ind}(\mathcal{B}_{i})\subseteq\mathsf{img}(h^{*})$;

  3. 3.

$\mathcal{B}_{i+1},\bar{a}_{1}\otimes\bar{a}_{2}\rightarrow\mathcal{B}_{i},\bar{a}_{1}\otimes\bar{a}_{2}$.

###### Proof.

We prove Point 1 by induction on $i$. For $i=1$, observe that either
$\mathcal{B}_{1}=\mathcal{C}^{3}_{\mathcal{A}_{1},\mathcal{O}}\times\mathcal{C}^{3}_{\mathcal{A}_{2},\mathcal{O}}$,
or $\mathcal{B}_{1}=\mathcal{A}_{q^{\bot}}$. In the first case both
$\mathcal{C}^{3}_{\mathcal{A}_{i},\mathcal{O}}$ are $\mathcal{O}$-saturated
and thus also their product by Lemma 5 Point 3. In the second case,
$\mathcal{A}_{q^{\bot}}$ is $\mathcal{O}$-saturated since it contains
$A(x_{0})$ for all concept names $A\in\Sigma$. For the induction step, suppose
$\mathcal{B}_{i+1},\mathcal{O}\models A(a)$ for some concept name $A$ and some
$a\in\mathsf{ind}(\mathcal{B}_{i+1})$. By monotonicity,
$\mathcal{B}^{\prime}_{i},\mathcal{O}\models A(a)$ where
$\mathcal{B}^{\prime}_{i}$ is the result of applying the unraveling step to
$\mathcal{B}_{i}$. By Point 2 of Lemma 3,
$A(a)\in\mathcal{U}_{\mathcal{B}^{\prime}_{i},\mathcal{O}}$. We distinguish
cases:

  * •

If $a\in\mathsf{ind}(\mathcal{B}_{i})$, then $a$ was not affected by the
unraveling and $\mathcal{B}_{i}^{\prime},a\preceq\mathcal{B}_{i},a$ by Lemma
21, thus
$\mathcal{U}_{\mathcal{B}_{i}^{\prime},\mathcal{O}},a\preceq\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}},a$
by Lemma 7. Hence $A(a)\in\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ and
$\mathcal{B}_{i},\mathcal{O}\models A(a)$ by Point 2 of Lemma 3. Induction
yields $A(a)\in\mathcal{B}_{i}$ and thus $A(a)\in\mathcal{B}_{i+1}$.

  * •

If $a\notin\mathsf{ind}(\mathcal{B}_{i})$, then $a$ is the copy of some
element $b\in\mathsf{ind}(\mathcal{B}_{i})$. By Lemma 21,
$\mathcal{B}_{i}^{\prime},a\preceq\mathcal{B}_{i},b$ and thus
$\mathcal{U}_{\mathcal{B}_{i}^{\prime},\mathcal{O}},a\preceq\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}},b$
by Lemma 7. Hence $A(b)\in\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ and
$\mathcal{B}_{i},\mathcal{O}\models A(b)$ by Point 2 of Lemma 3. Induction
yields $A(b)\in\mathcal{B}_{i}$ and the definition of unraveling implies
$A(a)\in\mathcal{B}_{i+1}$.

For Point 2, let $h$ be a homomorphism from $q_{T}$ to
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ with
$h(\bar{x})=\bar{a}_{1}\otimes\bar{a}_{2}$ for some $i\geq 2$. Assume to the
contrary of what is to be shown that there is an
$a\in\mathsf{ind}(\mathcal{B}_{i})$ that is not in $\mathsf{img}(h^{*})$. Let
$\mathcal{B}^{\prime}$ be the result of removing from $\mathcal{B}_{i}$ all
assertions that involve $a$. We show that

  * ($*$)

$h$ is a homomorphism from $q_{T}$ to
$\mathcal{U}_{\mathcal{B}^{\prime},\mathcal{O}}$

and thus witnesses that $\mathcal{B}^{\prime},\mathcal{O}\models
q_{T}(\bar{a}_{1}\otimes\bar{a}_{2})$. Hence, $a$ is dropped during the
Minimize step, in contradiction to $a\in\mathsf{ind}(\mathcal{B}_{i})$.

To see that $(*)$ holds, first note that for all
$b,b^{\prime}\in\mathsf{ind}(\mathcal{B}_{i})\setminus\\{a\\}$, the following
holds by Point 1 and construction of universal models:

  1. 1.

$A(b)\in\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ iff
$A(b)\in\mathcal{U}_{\mathcal{B}^{\prime},\mathcal{O}}$;

  2. 2.

$r(b,b^{\prime})\in\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ iff
$r(b,b^{\prime})\in\mathcal{U}_{\mathcal{B}^{\prime},\mathcal{O}}$.

From Point 1, in turn, it follows that the subtree in
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ below each
$b\in\mathsf{ind}(\mathcal{B}_{i})\setminus\\{a\\}$ is identical to the
subtree in $\mathcal{U}_{\mathcal{B}^{\prime},\mathcal{O}}$ below $b$. In
summary, ($*$) follows.

Now for Point 3, we define a mapping $h$ from $\mathcal{B}_{i+1}$ to
$\mathcal{B}_{i}$ with $h(\bar{x})=\bar{x}$. Recall that $\mathcal{B}_{i+1}$
is constructed from $\mathcal{B}_{i}$ by applying the Unravel and Minimize
steps. Let $h(s)=a$ for all
$a\in\mathsf{ind}(\mathcal{B}_{i})\cap\mathsf{ind}(\mathcal{B}_{i+1})$ and
$h(a^{\prime})=a$ for all copies $a^{\prime}$ of $a$ with
$a^{\prime}\in\mathsf{ind}(\mathcal{B}_{i+1})$. It follows from the definition
of the unravelling step, that $h$ is a homomorphism as required. ∎

It is proved as part of Lemma 25 below that the Unravel/Minimize phase
terminates after polynomially many steps, let $\mathcal{B}_{n}$ be the result.
We next construct a sequence $\mathcal{B}_{n},\mathcal{B}_{n+1},\dots$ using
the modified version of the original $\mathsf{refine}$ subroutine, that is,
using the Expand and Minimize steps. With $\mathcal{B}_{i}^{\prime}$, $i\geq
n$, we denote the result of only applying the Expand step to
$\mathcal{B}_{i}$, but not the Minimize step.

######  Lemma 24.

For all $i\geq n$,

  1. 1.

$\mathcal{B}_{i},\mathcal{O}\models q_{T}(\bar{a}_{1}\otimes\bar{a}_{2})$;

  2. 2.

$\mathcal{B}_{i}$ is $\mathcal{O}$-saturated;

  3. 3.

if $h$ is a homomorphism from $q_{T}$ to
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ with
$h(\bar{y})=\bar{a}_{1}\otimes\bar{a}_{2}$, then
$\mathsf{ind}(\mathcal{B}_{i})\subseteq\mathsf{img}(h^{*})$;

  4. 4.

$\mathcal{B}_{i+1},\bar{a}_{1}\otimes\bar{a}_{2}\to\mathcal{B}_{i},\bar{a}_{1}\otimes\bar{a}_{2}$.

  5. 5.

$|\mathsf{ind}(\mathcal{B}_{i+1})|>|\mathsf{ind}(\mathcal{B}_{i})|$.

###### Proof sketch..

Point 1 is a direct consequence of Lemma 13. Points 2 to 4 can be proved in
the same way as Points 1 to 4 of Lemma 14. While the proofs of Points 2 and 5
go through without modification, a slight extension is required for the proof
of Point 3 in the case that $i>1$. There, we start with a homomorphism $h$
from $q_{T}$ to $\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ with
$h(\bar{x})=\bar{b}_{i}$, and suppose that there is an
$a\in\mathsf{ind}(\mathcal{B}_{i})$ that is not in $\mathsf{img}(h^{*})$. If
$a$ is not reachable from some individual in
$\mathsf{ind}(\mathcal{A}_{1})\times\mathsf{ind}(\mathcal{A}_{2})$ in
$\mathcal{B}_{i}$ viewed as a directed graph, then we can argue as in the
proof of Point 2 of Lemma 14, that is, obtain a contradiction against
exhaustive application of Minimize to $\mathcal{B}_{i-1}$. If $a$ is
reachable, however, this does not work as we do not apply the Minimize step to
such individuals in the modified version of the $\mathsf{refine}$ subroutine.

However, by Point 4, there is a homomorphism $h$ from $\mathcal{B}_{i}$ to
$\mathcal{B}_{1}$ with
$h(\bar{a}_{1}\otimes\bar{a}_{2})=\bar{a}_{1}\otimes\bar{a}_{2}$. By Point 1
there is a homomorphism $h_{1}$ from $q_{T}$ to
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ with
$h_{1}(\bar{x})=\bar{a}_{1}\otimes\bar{a}_{2}$. Let $h_{2}$ be the extension
of $h$ to a homomorphism from $\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ to
$\mathcal{U}_{\mathcal{B}_{1},\mathcal{O}}$ as in Lemma 7 Point 1. Then
$\mathsf{img}(h_{2}^{*})=\mathsf{img}(h)$. Composing $h_{1}$ and $h_{2}$
yields a homomorphism $h_{3}$ from $q_{T}$ to
$\mathcal{U}_{\mathcal{B}_{i},\mathcal{O}}$ with
$h_{3}(\bar{x})=\bar{a}_{1}\otimes\bar{a}_{2}$, but with
$\mathsf{ind}(\mathcal{B}_{i})\not\subseteq\mathsf{img}(h_{3}^{*})$, in
contradiction to Point 2 of Lemma 23. ∎

######  Lemma 25.

$\mathsf{refine}(q(\bar{x}))$ can be computed in time polynomial in
$||q_{T}||+||q||$ using membership queries.

###### Proof.

We first note that the length of the sequence
$\mathcal{B}_{1},\mathcal{B}_{2},\ldots$ computed in the Unravel/Minimize
phase is bounded by $|\mathsf{var}(q_{T})|+1$. Indeed, the following is easy
to prove by induction on $i$.

Claim. Let $i\geq 1$. Then every individual in $\mathcal{B}_{i}$ that is
reachable in the directed graph
$G_{\mathcal{B}_{i}}=(\mathsf{ind}(\mathcal{B}_{i}),\\{(a,b)\mid
r(a,b)\in\mathcal{B}_{i}\\})$ from some individual in
$\mathsf{ind}(\mathcal{A}_{1})\times\mathsf{ind}(\mathcal{A}_{2})$ on a path
of length at most $i-1$ is unraveled.

Since every individual in $\mathcal{B}_{i}$ that is reachable from some
individual in
$\mathsf{ind}(\mathcal{A}_{1})\times\mathsf{ind}(\mathcal{A}_{2})$ is
reachable on a path of length at most $|\mathsf{ind}(\mathcal{B}_{i})|$ and
$|\mathsf{ind}(\mathcal{B}_{i})|\leq|\mathsf{var}(q_{T})|$ by Point 2 of Lemma
23, it follows that the Unravel step is thus no longer applicable to
$\mathcal{B}_{m+2}$ for $m=|\mathsf{var}(q_{T})|$.

Next observe that the length of the sequence
$\mathcal{B}_{n},\mathcal{B}_{n+1}$ computed in the Expand/Minimize phase is
also bounded by $|\mathsf{var}(q_{T})|$ as we have for all $i\geq n$,
$|\mathsf{ind}(\mathcal{B}_{i})|\leq|\mathsf{var}(q_{T})|$, by Lemma 24 Point
3, and $|\mathsf{ind}(\mathcal{B}_{i})|<|\mathsf{ind}(\mathcal{B}_{i+1})|$, by
Lemma 24 Point 5.

It remains to show that every step runs in polynomial time. First note that,
for all $i\geq 1$, we have
$|\mathsf{ind}(\mathcal{B}_{i})|\leq|\mathsf{var}(q_{T})|$ by Lemma 23 Point 2
and Lemma 24 Point 3. Moreover, by definition of the Unravel/Minimize steps,
we have $\mathsf{sig}(\mathcal{B}_{i})\subseteq\Omega$, for all $i$, where
$\Omega=\mathsf{sig}(q)$ and thus $|\Omega|\leq||q||$. Applying the Unravel
step to $\mathcal{B}_{i}$ thus takes time polynomial in
$|\mathsf{ind}(\mathcal{B}_{i})|$ and $|\Omega|$. The resulting ABox
$\mathcal{B}^{\prime}$ is such that
$|\mathsf{ind}(\mathcal{B}^{\prime})|\leq|\mathsf{ind}(\mathcal{B}_{i})|^{2}\cdot|\Omega|$.
The number of membership queries needed in the minimization step is thus
bounded by $|\mathsf{var}(q_{T})|^{2}\cdot||q||$.

For Expand, note that chordless cycles of length $n>n_{\text{max}}$ can be
identified in time polynomial in
$|\mathsf{ind}(\mathcal{B}_{i})|\leq|\mathsf{var}(q_{T})|$ and constructing
the ABox $\mathcal{B}_{i+1}$ from $\mathcal{B}_{i}$ is clearly also possible
in polynomial time. ∎

######  Lemma 26.

Let $\mathcal{O}$ be an ${\cal E\\!\\!\>L}^{r}$-ontology. Let
$\mathcal{A}_{1}$ and $\mathcal{A}_{2}$ be ABoxes and $\bar{a}_{i}$,
$i\in\\{1,2\\}$, be tuples of individuals from $\mathcal{A}_{i}$ of the same
length. Moreover, let $q(\bar{z})$ be
$\mathcal{C}^{3}_{\mathcal{A}_{1},\mathcal{O}}\times\mathcal{C}^{3}_{\mathcal{A}_{2},\mathcal{O}}$
viewed as CQ with answer variables $\bar{z}=\bar{a}_{1}\otimes\bar{a}_{2}$ and
let $p(\bar{x})$ be the result of $\mathsf{refine}(q(\bar{z}))$ with respect
to some target query $q_{T}(\bar{y})$. Then there is a homomorphism $h_{i}$
from $p(\bar{x})$ to $\mathcal{U}_{\mathcal{A}_{i},\mathcal{O}}$ with
$h_{i}(\bar{x})=(\bar{a}_{i})$, for $i\in\\{1,2\\}$.

###### Proof.

Let $\mathcal{B}_{m}$ be the result of $\mathsf{refine}(q(\bar{z}))$ before it
is turned into the CQ $p(\bar{x})$. Further, let $\mathcal{B}^{\prime}$ denote
the restriction of $\mathcal{B}_{m}$ to all individuals that are reachable
from an individual in
$\mathsf{ind}(\mathcal{A}_{1})\times\mathsf{ind}(\mathcal{A}_{2})$ in
$\mathcal{B}_{m}$, and let $\mathcal{B}^{\prime\prime}$ be the restriction of
$\mathcal{B}_{m}$ to all individuals that are not reachable. Thus
$\mathcal{B}_{m}=\mathcal{B}^{\prime}\uplus\mathcal{B}^{\prime\prime}$.

It suffices to show that, for $i\in\\{1,2\\}$, there is a homomorphism
$h^{\prime}_{i}$ from $\mathcal{B}^{\prime}$ to
$\mathcal{U}_{\mathcal{A}_{i},\mathcal{O}}$ with
$h^{\prime}_{i}(\bar{x})=(\bar{a}_{i})$ and a homomorphism
$h^{\prime\prime}_{i}$ from $\mathcal{B}^{\prime\prime}$ to
$\mathcal{U}_{\mathcal{A}_{i},\mathcal{O}}$.

For the former, note that all individuals in $\mathcal{B}^{\prime}$ are
unraveled. Thus
$\mathcal{B}^{\prime}\subseteq\mathcal{U}_{\mathcal{A}_{1},\mathcal{O}}\times\mathcal{U}_{\mathcal{A}_{2},\mathcal{O}}$
and the identity is a homomorphism $h^{\prime}$ from $\mathcal{B}$ to
$\mathcal{U}_{\mathcal{A}_{1},\mathcal{O}}\times\mathcal{U}_{\mathcal{A}_{2},\mathcal{O}}$
with $h^{\prime}(\bar{b})=\bar{a}_{1}\times\bar{a}_{2}$. Projection to the
left and right components yields the homomorphisms $h^{\prime}_{i}$ as
required.

For the latter, note that none of the individuals in
$\mathcal{B}^{\prime\prime}$ is unraveled. In fact, this follows from two
obvious properties of the Unravel step and 3-compact canonical models:

  * •

if the Unravel step is not applicable to an ABox $\mathcal{B}_{i}$ and
$r(a,b)\in\mathcal{B}_{i}$ with $a$ unraveled, then $b$ is unraveled too;

  * •

if Unraveling (and Minimization) is repeatedly applied to an ABox
$\mathcal{C}^{3}_{\mathcal{A}_{1},\mathcal{O}}\times\mathcal{C}^{3}_{\mathcal{A}_{2},\mathcal{O}}$,
then it never produces any fact $r(a,b)$ with $b$ unraveled, but $a$ not
unraveled (because there are no $r$-edges from individuals of the form
$c_{a,i,s,C}$ to individuals from $\mathsf{ind}(\mathcal{A}_{i})$ in
$\mathcal{C}^{3}_{\mathcal{A}_{i},\mathcal{O}}$.

Thus, the identity is a homomorphism from $\mathcal{B}^{\prime\prime}$ viewed
as a Boolean CQ to
$\mathcal{C}^{3}_{\mathcal{A}_{1},\mathcal{O}}\times\mathcal{C}^{3}_{\mathcal{A}_{2},\mathcal{O}}$.
Projection to the left and right components yields a homomorphism
$g^{\prime\prime}_{i}$ from $\mathcal{B}^{\prime\prime}$ to
$\mathcal{C}^{3}_{\mathcal{A}_{i},\mathcal{O}}$ for $i\in\\{1,2\\}$. By
definition of the Expansion and Minimize step and its use in
$\mathsf{refine}$, it is clear that $\mathcal{B}^{\prime\prime}$ is chordal.
From Lemma 2, it thus follows that $\mathcal{B}^{\prime\prime}$ viewed as a CQ
is an ELIQ. Using the construction of
$\mathcal{C}^{3}_{\mathcal{A}_{i},\mathcal{O}}$ and
$\mathcal{U}_{\mathcal{A}_{i},\mathcal{O}}$, it is now straightforward to
convert the homomorphism $g^{\prime\prime}_{i}$ from ELIQ
$\mathcal{B}^{\prime\prime}$ to
$\mathcal{C}^{3}_{\mathcal{A}_{i},\mathcal{O}}$ into the desired homomorphism
$h^{\prime\prime}_{i}$ from $\mathcal{B}^{\prime\prime}$ to
$\mathcal{U}_{\mathcal{A}_{i},\mathcal{O}}$. ∎

##  Appendix G Proof of Theorem 1

Let $q_{0}(\bar{x}_{0}),q_{1}(\bar{x}_{1}),\ldots$ be the sequence of
hypotheses generated by the algorithm.

######  Lemma 27.

For all $i\geq 0$:

  1. 1.

$q_{i}\subseteq_{\mathcal{O}}q_{T}$;

  2. 2.

$q_{i}\subseteq_{\mathcal{O}}q_{i+1}$;

  3. 3.

$q_{i+1}\not\subseteq_{\mathcal{O}}q_{i}$.

###### Proof.

Point 1 is a consequence of Lemma 13 Point 1, for the first
$\mathsf{refine}$-operation, and Lemma 24 Point 1, for the second
$\mathsf{refine}$-operation

For Point 2, recall that $q_{i+1}=\mathsf{refine}(q_{H}^{\prime}(\bar{x}))$
where $q_{H}^{\prime}(\bar{x})$ is
$\mathcal{C}^{3}_{\mathcal{A}_{q_{i}},\mathcal{O}}\times\mathcal{C}^{3}_{\mathcal{A},\mathcal{O}}$,
for some positive counterexample $\mathcal{A},\bar{a}$, viewed as CQ with
answer variables $\bar{x}=\bar{x}_{i}\otimes\bar{a}$. In case of the first
$\mathsf{refine}$-operation there is a homomorphism $h$ from $q_{i+1}$ to
$\mathcal{U}_{\mathcal{A}_{q_{i}},\mathcal{O}}$ with $h(\bar{x}_{i+1})=x_{i}$,
by Lemma 19. Lemmas 22 and 24 Point 4 give us this homomorphism for the second
$\mathsf{refine}$-operation. By Lemma 4, we obtain
$q_{i}\subseteq_{\mathcal{O}}q_{i+1}$.

For Point 3, assume to the contrary that
$q_{i+1}\subseteq_{\mathcal{O}}q_{i}$. Then there is a homomorphism $h_{1}$
from $q_{i}$ to $\mathcal{U}_{\mathcal{A}_{q_{i+1}},\mathcal{O}}$ with
$h_{1}(\bar{x}_{i})=\bar{x}_{i+1}$. Recall once more that
$q_{i+1}=\mathsf{refine}(q_{H}(\bar{x}))$ where $q_{H}(\bar{x})$ is
$\mathcal{C}^{3}_{\mathcal{A}_{q_{i}},\mathcal{O}}\times\mathcal{C}^{3}_{\mathcal{A},\mathcal{O}}$,
for some positive counterexample $\mathcal{A},\bar{a}$, viewed as CQ with
answer variables $\bar{x}=\bar{x}_{i}\otimes\bar{a}$. In case of the first
$\mathsf{refine}$-operation there is a homomorphism $h_{2}$ from $q_{i+1}$ to
$\mathcal{U}_{\mathcal{A},\mathcal{O}}$ with $h_{2}(\bar{x}_{i+1})=\bar{a}$,
by Lemma 19. Again, Lemmas 22 and 24 show that $h_{2}$ also exists for the
second$\mathsf{refine}$-operation. By Lemma 7 Point 1 $h_{2}$ can be extended
to a homomorphism $h_{2}^{\prime}$ from
$\mathcal{U}_{\mathcal{A}_{q_{i+1}},\mathcal{O}}$ to
$\mathcal{U}_{\mathcal{A},\mathcal{O}}$ with
$h_{2}^{\prime}(\bar{x}_{i+1})=\bar{a}$. Composing $h_{1}$ and $h_{2}$ yields
a homomorphism $h$ from $q_{i}$ to $\mathcal{U}_{\mathcal{A},\mathcal{O}}$
with $h(\bar{x})=\bar{a}$. Thus $\mathcal{A},\mathcal{O}\models
q_{i}(\bar{a})$, in contradiction to $\mathcal{A},\bar{a}$ being a positive
counterexample. ∎

We next observe that the sizes of $q_{0},q_{1},\ldots$ are non-decreasing.

######  Lemma 28.

For all $i\geq 0$:

  1. 1.

$\mathsf{var}(q_{i})\subseteq\mathsf{img}(h^{*})$ for every homomorphism $h$
from $q_{i+1}$ to $\mathcal{U}_{\mathcal{A}_{q_{i}},\mathcal{O}}$ with
$h(\bar{x}_{i+1})=\bar{x}_{i}$;

  2. 2.

$|\mathsf{var}(q_{i})|\leq|\mathsf{var}(q_{i+1})|$;

###### Proof.

For Point 1, let $h$ be a homomorphism from $q_{i+1}$ to
$\mathcal{U}_{\mathcal{A}_{q_{i}},\mathcal{O}}$ with
$h(\bar{x}_{i+1})=\bar{x}_{i}$. By Lemma 7 Point 1, we can extend $h$ to a
homomorphism from $\mathcal{U}_{\mathcal{A}_{q_{i+1}},\mathcal{O}}$ to
$\mathcal{U}_{\mathcal{A}_{q_{i}},\mathcal{O}}$ without adding individuals
from $\mathsf{var}(q_{i})$ to $\mathsf{img}(h^{*})$. By Point 1 of Lemma 27,
there is a homomorphism $h^{\prime}$ from $q_{T}$ to
$\mathcal{U}_{\mathcal{A}_{q_{i+1}},\mathcal{O}}$ with
$h(\bar{x})=\bar{x}_{i+1}$. We can compose $h^{\prime}$ and $h$ into a
homomorphism $g$ from $q_{T}$ to
$\mathcal{U}_{\mathcal{A}_{q_{i}},\mathcal{O}}$ with $g(\bar{x})=\bar{x}_{i}$.
We then obtain $\mathsf{var}(q_{i})\subseteq\mathsf{img}(g^{*})$ by Lemma 14
Point 2 for the first $\mathsf{refine}$-operation or Lemma 24 for the second
version. Since $\mathsf{img}(g^{*})\subseteq\mathsf{img}(h^{*})$, it follows
that $\mathsf{var}(q_{i})\subseteq\mathsf{img}(h^{*})$.

Point 2 is a consequence of Point 1. In fact,
$q_{i}\subseteq_{\mathcal{O}}q_{i+1}$ implies via Lemma 4 that there is a
homomorphism $h$ from $q_{i+1}$ to
$\mathcal{U}_{\mathcal{A}_{q_{i}},\mathcal{O}}$ with
$h(\bar{x}_{i+1})=\bar{x}_{i}$. Point 1 yields
$\mathsf{var}(q_{i})\subseteq\mathsf{img}(h^{*})$ and thus
$|\mathsf{var}(q_{i})|\leq|\mathsf{var}(q_{i+1})|$. ∎

######  Lemma 29.

$q_{i}\equiv_{\mathcal{O}}q_{T}$ for some $i\leq
p(|\mathsf{var}(q_{T})|+|\Sigma|)$ for some polynomial $p$.

###### Proof.

By Lemma 14 Point 2 in case of the first $\mathsf{refine}$-operation or by
Lemma 24 Point 3 in case of the second, we have
$|\mathsf{var}(q_{i})|\leq|\mathsf{var}(q_{T})|$ for all $i\geq 0$.

Let $q_{\ell},\dots,q_{u}$, $\ell\leq u$, be a subsequence of
$q_{1},q_{2},\ldots$ such that
$|\mathsf{var}(q_{\ell})|=\cdots=|\mathsf{var}(q_{u})|$. By Point 2 of Lemma
28, it suffices to show that the length $u-\ell$ of any such sequence is
bounded by a polynomial in $|\mathsf{var}(q_{T})|$ and $|\Sigma|$. Let
$h_{i}$, for $i\in\\{\ell+1,\ldots,u\\}$, be the homomorphisms from $q_{i}$ to
$\mathcal{U}_{\mathcal{A}_{q_{i-1}},\mathcal{O}}$ that exist due to Lemma 27
Point 2.

Note that $h^{*}_{i}$ is a bijection between $\mathsf{var}(q_{i})$ and
$\mathsf{var}(q_{i-1})$. Denote with $V_{i}$ the set of all quantified
variables $x\in\mathsf{var}(q_{i})$ which do not occur in a role atom, and
define $U_{i}=\mathsf{var}(q_{i})\setminus V_{i}$. Let us further denote with
$q^{x}$ the restriction $q|_{\\{x\\}}$ of a query $q$ to a single variable
$x\in\mathsf{var}(q)$. Clearly, $q_{i}$ can be written as

$q_{i}(\bar{x}_{i})\leftarrow q_{i}|_{U_{i}}\wedge\bigwedge_{x\in
V_{i}}q_{i}^{x}$

Notice that, by definition, each $q_{i}^{x}$, $x\in V_{i}$ is a query without
answer variables.

Claim 1. $x\in U_{i}$ implies $h_{i}^{*}(x)\in U_{i-1}$.

Proof of Claim 1. Let $x\in U_{i}$. If $x$ is an answer variable then
$h_{i}(x)=h^{*}_{i}(x)$ is an answer variable and thus in $U_{i-1}$. Suppose
now that there is a role atom $R(z,x)$ in $q_{i}$ and consider the assertion
$R(h_{i}(z),h_{i}(x))\in\mathcal{U}_{\mathcal{A}_{q_{i-1}},\mathcal{O}}$ which
exists since $h_{i}$ is a homomorphism. Since $h^{*}_{i}$ is a bijection,
$z=x$ or $h^{*}_{i}(z)\neq h^{*}_{i}(x)$.

  * •

In the first case, we obtain
$R(y,y)\in\mathcal{U}_{\mathcal{A}_{q_{i-1}},\mathcal{O}}$ for
$y=h_{i}(z)=h_{i}(x)$. The definition of the universal models yields
$y\in\mathsf{var}(q_{i-1})$, $R(y,y)$ occurs in $q_{i-1}$, and
$h_{i}^{*}(z)=h_{i}(z)\in U_{i-1}$.

  * •

In the second case, we obtain $h^{*}_{i}(z)=h_{i}(z)\in\mathsf{var}(q_{i-1})$,
$h^{*}_{i}(x)=h_{i}(x)\in\mathsf{var}(q_{i})$, and $R(h_{i}(z),h_{i}(x))$
occurs in $q_{i-1}$. Hence, $x\in U_{i-1}$.

This finishes the proof of Claim 1.

Claim 1 implies $|U_{i}|\leq|U_{i-1}|$ for every $i\in\\{\ell+1,\ldots,u\\}$.
We consider now subsequences $q_{\ell^{\prime}},\ldots,q_{u^{\prime}}$ of
$q_{\ell},\ldots,q_{u}$ with $|U_{\ell^{\prime}}|=\dots=|U_{u^{\prime}}|$ and
thus $|V_{\ell^{\prime}}|=\dots=|V_{u^{\prime}}|$. Since
$|U_{i}|\leq|\mathsf{var}(q_{T})|$, for all $i$, it suffices to show that the
length of such a sequence is bounded by a polynomial in
$|\mathsf{var}(q_{T})|$ and $|\Sigma|$.

Claim 2. For every $i\in\\{\ell^{\prime}+1,\ldots,u^{\prime}\\}$,

  1. 1.

$h_{i}^{*}$ is a bijection between $V_{i}$ and $V_{i-1}$, and

  2. 2.

$h_{i}$ is a bijection between $U_{i}$ and $U_{i-1}$.

Proof of Claim 2. The first point is a consequence of Claim 1 and the facts
that $|V_{i-1}|=|V_{i}|$ and $h^{*}_{i}$ is a bijection between
$\mathsf{var}(q_{i})$ and $\mathsf{var}(q_{i-1})$. For the second point,
suppose that some $x\in U_{i-1}$ is not $h_{i}(y)$ for some $y\in U_{i}$.
Thus, there is some $y$ such that $h^{*}_{i}(y)=x$ and $h_{i}(y)$ is strictly
in the subtree rooted at $x$ in
$\mathcal{U}_{\mathcal{A}_{q_{i-1}},\mathcal{O}}$. Since $h_{i}^{*}$ is a
bijection, $y$ is the unique variable such that $h_{i}(y)$ is in the subtree
rooted at $x$. We claim that $y\in V_{i}$. This implies $x\in V_{i-1}$, by the
first point, and contradicts the assumption $x\in U_{i-1}$. To see $y\in
V_{i}$, suppose the contrary, that is, $y\in U_{i}$. If $y$ is an answer
variable, then $h_{i}(y)$ is an answer variable and thus in $U_{i}$,
contradiction. Otherwise, there is some $R(y,z)$ in $q_{i}$. Since $h_{i}(y)$
is _strictly_ below $x$, this leads to a contradiction as follows. If $z\neq
y$, then $h^{*}_{i}(z)=h^{*}_{i}(y)$ contradicts the fact that $h_{i}^{*}$ is
a bijection. If, on the other hand, $z=y$, then $h_{i}$ is not a homomorphism
since there is no self-loop $R(h_{i}(y),h_{i}(y))$ in
$\mathcal{U}_{\mathcal{A}_{q_{i-1}},\mathcal{O}}$, by definition of the
universal model. This finishes the proof of Claim 2.

Sanctioned by the first point in Claim 2, in what follows we assume for the
sake of readability that $h_{i}^{*}(x)=x$ for all $x\in V_{i}$ and
$i\in\\{\ell^{\prime}+1,\ldots,u^{\prime}\\}$. Hence,
$V_{\ell^{\prime}}=\dots=V_{u^{\prime}}$. Now, observe that, for all
$i\in\\{\ell^{\prime}+1,\ldots,u^{\prime}\\}$, one of the following is the
case:

  1. 1.

the inverse of $h_{i}$ is not a homomorphism from $q_{i-1}|_{U_{i-1}}$ to
$q_{i}|_{U_{i}}$;

  2. 2.

there is some $x\in V_{i}$ such that
$q_{i}^{x}\not\subseteq_{\mathcal{O}}q_{i-1}^{x}$.

Indeed, if neither Point 1 nor Point 2 is satisfied then
$q_{i}\equiv_{\mathcal{O}}q_{i-1}$, in contradiction to Point 3 of Lemma 27.
It thus remains to bound the number of times each of these points can be
satisfied along $q_{\ell^{\prime}},\ldots,q_{u^{\prime}}$. We start with Point
1.

Claim 3. The number of $i\in\\{\ell^{\prime}+1,\ldots,u^{\prime}\\}$ such that
the inverse of $h_{i}$ is not a homomorphism from $q_{i-1}|_{U_{i-1}}$ to
$q_{i}|_{U_{i}}$ is at most
$(|\mathsf{var}(q_{T})|^{2}+|\mathsf{var}(q_{T})|)\cdot|\Sigma|$.

Proof of Claim 3. Let $i$ be as in the claim. By Point 2 of Claim 2, $h_{i}$
is a bijective homomorphism from $q_{i}|_{U_{i}}$ to $q_{i-1}|_{U_{i-1}}$.
Hence, the number $n_{i}$ of atoms in $q_{i}|_{U_{i}}$ is at most the number
$n_{i-1}$ of atoms in $q_{i-1}|_{U_{i-1}}$. As the inverse of $h_{i}$ is not a
homomorphism, we have $n_{i}<n_{i-1}$. Since the maximal number of atoms in
$q_{i}$ is bounded by
$|\Sigma|\cdot|\mathsf{var}(q_{T})|^{2}+|\Sigma|\cdot|\mathsf{var}(q_{T})|$,
the claim follows.

Now for Point 2.

Claim 4. Let $x\in V_{\ell^{\prime}}$. The number of
$i\in\\{\ell^{\prime}+1,\ldots,u^{\prime}\\}$ such that
$q_{i}^{x}\not\subseteq_{\mathcal{O}}q_{i-1}^{x}$ is at most $|\Sigma|^{2}$.

Proof of Claim 4. Let $I$ be the set of all $i$ as in the claim. Let $i\in I$.
We distinguish two cases.

  1. (A)

$h_{i}(x)=x$.

Since $h_{i}$ is a homomorphism, the number $n_{i}$ of atoms in $q_{i}^{x}$ is
at most the number $n_{i-1}$ of atoms in $q_{i-1}^{x}$. From
$q_{i-1}^{x}\not\subseteq_{\mathcal{O}}q_{i}^{x}$, it follows that
$n_{i}<n_{i-1}$.

  2. (B)

$h_{i}(x)\neq x$, that is, $h_{i}(x)$ is strictly in the subtree below $x$.

By definition of the universal model and since $\mathcal{O}$ is in normal
form, there is an atom $A(x)$ in $q_{i-1}^{x}$ such that there is a
homomorphism from $q_{i}^{x}$ to $\mathcal{U}_{\\{A(a)\\},\mathcal{O}}$. We
claim that $A(x)$ is not an atom in any query $q_{j}^{x}$ with $j>i$ and $j\in
I$. Indeed, if $A(x)$ occurs in $q_{j}^{x}$ for such $j$, then
$q_{j}^{x}\subseteq_{\mathcal{O}}q_{i}^{x}$. The homomorphisms
$h_{i+1},\ldots,h_{j}$ witness that
$q_{i}^{x}\subseteq_{\mathcal{O}}q_{i+1}^{x}\subseteq_{\mathcal{O}}\cdots\subseteq_{\mathcal{O}}q_{j}^{x}$,
and thus all these queries are actually equivalent, in contradiction to the
definition of $I$.

Next observe that, by what was said in Point (A), Point (A) can happen only
$|\Sigma|$ times without Point (B) happening in between. Moreover, Point (B)
can happen only $|\Sigma|$ times overall. We thus have that the size of $I$ is
bounded by $|\Sigma|^{2}$. This finishes the proof of Claim 4.

Since $|V_{\ell^{\prime}}|\leq|\mathsf{var}(q_{T})|$, we obtain that the
length of the sequence $q_{\ell^{\prime}},\ldots,q_{u^{\prime}}$ is bounded by

$\displaystyle\big{(}(|\mathsf{var}(q_{T})|^{2}+|\mathsf{var}(q_{T})|)\cdot|\Sigma|\big{)}+|\mathsf{var}(q_{T})|\cdot|\Sigma|^{2}.$

where the first summand accomodates the number of $i$ where Point 1 is
satisfied and the second summand accomodates the number of $i$ where Point 2
is satisfied. ∎

##  Appendix H Proofs for Section 4

See 3

###### Proof.

Assume to the contrary of what is to be shown that ${\cal
E\\!\\!\>L}$-concepts are polynomial query learnable under ${\cal
E\\!\\!\>LI}$-ontologies when unrestricted CQs can be used in equivalence
queries. Then there exists a learning algorithm and a polynomial $p$ such that
at any time, the sum of the sizes of the inputs to membership and equivalence
queries made so far is bounded by $p(n_{1},n_{2},n_{3})$, where $n_{1}$ is the
size of $C_{T}$, $n_{2}$ is the size of $\mathcal{O}$, and $n_{3}$ is the size
of the largest counterexample seen so far.

We choose $n$ such that $2^{n}>p(q_{1}(n),q_{2}(n),q_{3}(n))+1$ where
$q_{1},q_{2},q_{3}$ are polynomials such that for every $n\geq 1$,
$q_{1}(n)\geq||H||$ for all $H\in\mathcal{H}_{n}$,
$q_{2}(n)\geq||\mathcal{O}_{n}||$, and $q_{3}(n)$ bounds from above the size
of all counterexamples returned by the oracle that we craft below.

Consider now $\mathcal{O}_{n}$ and $\mathcal{H}_{n}$ as defined in Section 4.
We let the oracle maintain a set of hypotheses $\mathcal{H}$, starting with
$\mathcal{H}=\mathcal{H}_{n}$ and then proceeding to subsets thereof, in such
a way that at any point in time the learner cannot distinguish between any of
the candidate targets in $\mathcal{H}$.

More precisely, consider a membership query with ABox $\mathcal{A}$ and
individual $a_{0}$. The oracle responds as follows:

  1. 1.

if $\mathcal{A},\mathcal{O}_{n}\models L_{0}(a_{0})$, then answer yes;

  2. 2.

if $\mathcal{A},\mathcal{O}_{n}\models K_{0}(a_{0})$ and there are
$\sigma_{1},\dots,\sigma_{n}\in\\{r,s\\}$ with
$\mathcal{A},\mathcal{O}_{n}\models W^{\sigma_{i}}_{i}(a_{0})$ for $1\leq
i\leq n$, then answer yes and remove
$\exists\sigma_{1}\cdots\exists\sigma_{n}.\exists r^{n}.A$ from $\mathcal{H}$;

  3. 3.

otherwise, answer no and remove all $H$ with
$\mathcal{A},\mathcal{O}_{n}\models H(a_{0})$ from $\mathcal{H}$.

Higher up rules have higher priority, e.g., Case 2 is applied only if Case 1
does not apply. It is not hard to verify that the answers are correct
regarding the hypothesis set $\mathcal{H}$ that remains after the answer is
given.

Now consider an equivalence query with CQ $q_{H}(x_{0})$. The oracle responds
as follows:

  1. 1.

if $\\{L_{0}(a_{0})\\},\mathcal{O}_{n}\not\models q_{H}(a_{0})$, then return
$\\{L_{0}(a_{0})\\}$ as positive counterexample;

  2. 2.

if $\\{\top(a_{0}),L_{0}(a_{1})\\}\models q_{H}(a_{0})$, then return
$\\{\top(a_{0}),L_{0}(a_{1})\\}$ as negative counterexample;

  3. 3.

if there are $\sigma_{1},\dots,\sigma_{n}\in\\{r,s\\}$ such that

$\\{K_{0}(a_{0}),W^{\sigma_{1}}_{1}(a_{0}),\dots,W^{\sigma_{n}}_{n}(a_{0})\\},\mathcal{O}_{n}\not\models
q_{H}(a_{0}),$

then choose such $\sigma_{1},\dots,\sigma_{n}$, return

$\\{K_{0}(a_{0}),W^{\sigma_{1}}_{1}(a_{0}),\dots,W^{\sigma_{n}}_{n}(a_{0})\\}$

as positive counterexample, and remove
$\exists\sigma_{1}\cdots\exists\sigma_{n}.\exists r^{n}.A$ from $\mathcal{H}$
(if present).

Again, higher up rules have higher priority and the answers are always correct
with respect to the updated set $\mathcal{H}$. For Case 3, we remark that the
counterexample
$\mathcal{A}=\\{K_{0}(a_{0}),W^{\sigma_{1}}_{1}(a_{0}),\dots,W^{\sigma_{n}}_{n}(a_{0})\\}$
is such that
$\mathcal{A},\mathcal{O}_{n}\sqsubseteq\exists\sigma^{\prime}_{1}\cdots\exists\sigma^{\prime}_{n}.\exists
r^{n}.A(a_{0})$ for all
$\sigma^{\prime}_{1}\cdots\sigma^{\prime}_{n}\in\\{r,s\\}^{n}$ except
$\sigma^{\prime}_{1}\cdots\sigma^{\prime}_{n}=\sigma_{1}\cdots\sigma_{n}$.

We argue that the cases are exhaustive. Assume that Cases 1 and 2 do not
apply. Let $q^{\prime}_{H}$ be the restriction of $q_{H}$ to variables that
are reachable from $x_{0}$ in the undirected graph

$G_{q_{H}}=(\mathsf{var}(q_{H}),\\{\\{x,y\\}\mid t(x,y)\in q_{H}\\})$

and let $q^{\prime\prime}_{H}$ be the restriction of $q_{H}$ to the variables
that are not reachable.

Non-applicability of Case 1 implies that there is a homomorphism $h$ from
$q_{H}$ to $\mathcal{U}_{\\{L_{0}(a_{0})\\},\mathcal{O}_{n}}$ with
$h(x_{0})=a_{0}$. Consequently, $q_{H}$ can only contain the symbols $r$, $s$,
$A$ as well as the concept names $U_{i}^{\sigma}$. Moreover, if there is an
atom $A(x)$ in $q^{\prime}_{H}$, then $x$ is reachable from $x_{0}$ in
$G_{q_{H}}$ on an $r/s$-path of length exactly $2n$ whose last $n$ components
are all $r$.

We next show that $q^{\prime}_{H}$ contains an atom $A(x)$. If it does not, in
fact, then $h$ is also a homomorphism from $q^{\prime}_{H}$ to
$\mathcal{U}_{\\{\top(a_{0})\\},\mathcal{O}_{n}}$ due to the first CI in
$\mathcal{O}_{n}$, and we find a homomorphism $h^{\prime}$ from
$q^{\prime\prime}_{H}$ to $\mathcal{U}_{\\{L_{0}(a_{1})\\},\mathcal{O}_{n}}$.
Combining $h$ and $h^{\prime}$ yields a homomorphism $g$ from $q_{H}$ to
$\mathcal{U}_{\\{\top(a_{0}),L_{0}(a_{1})\\},\mathcal{O}_{n}}$ with
$g(x_{0})=a_{0}$, in contradiction to Case 2 not being applicable.

So $q^{\prime}_{H}$ contains an atom $A(x)$. As argued above, $x$ is then
reachable from $x_{0}$ along an $r/s$-path of length exactly $2n$ whose last
$n$ components are all $r$. Let the first $n$ components be
$\sigma_{1},\dots,\sigma_{n}$. Then

$\\{K_{0}(a_{0}),W^{\sigma_{1}}_{1}(a_{0}),\dots,W^{\sigma_{n}}_{n}(a_{0})\\},\mathcal{O}_{n}\not\models
q_{H}(a_{0})$

and thus Case 3 is applicable.

We next observe the following.

Claim. If $\mathcal{A}$ and $a_{0}$ were given as a membership query and Cases
1 and 2 of membership queries do not apply, then
$||\mathcal{A}||\geq|\\{H\in\mathcal{H}_{n}\mid\mathcal{A},\mathcal{O}_{n}\models
H(a_{0})\\}|$.

Proof of the claim. We may assume w.l.o.g. that $\mathcal{A}$ is connected,
that is, the undirected graph
$G_{\mathcal{A}}=(\mathsf{ind}(\mathcal{A}),\\{\\{a,b\\}\mid
t(a,b)\in\mathcal{A}\\})$ is connected. Since Cases 1 and 2 of membership
queries do not apply,

  * (a)

$\mathcal{A},\mathcal{O}_{n}\not\models L_{0}(a_{0})$ and

  * (b)

there are no $\sigma_{1},\dots,\sigma_{n}\in\\{r,s\\}$ such that
$\mathcal{A},\mathcal{O}_{n}\models K_{0}(a_{0})$ and
$\mathcal{A},\mathcal{O}_{n}\models W^{\sigma_{i}}_{i}(a_{0})$ for $1\leq
i\leq n$.

By the construction of $\mathcal{O}_{n}$, these properties imply the following
for $0\leq i\leq 2n$:

  * (c)

$\mathcal{A}$ contains no $r/s$-path of length $i$ from $a_{0}$ to some $a$
with $\mathcal{A},\mathcal{O}_{n}\models L_{i}(a)$.

In fact, the existence of such a path implies
$\mathcal{A},\mathcal{O}_{n}\models L_{0}(a_{0})$.

  * (d)

$\mathcal{A}$ contains no $r/s$-path of length $i$ from $a_{0}$ to some $a$
with $\mathcal{A},\mathcal{O}_{n}\models K_{i}(a)$ and assertions
$W^{\sigma_{1}}_{1}(a_{1}),\dots,W^{\sigma_{n}}_{n}(a_{n})$ where
$\sigma_{1},\dots,\sigma_{n}\in\\{r,s\\}$.

In fact, the existence of such a path and such assertions implies
$\mathcal{A},\mathcal{O}_{n}\models K_{0}(a_{0})$ and
$\mathcal{A},\mathcal{O}_{n}\models W^{\sigma_{i}}_{i}(a_{0})$ for $1\leq
i\leq n$.

  * (e)

$\mathcal{A}$ contains no $r/s$-paths $p_{1},p_{2}$ of length $i$ that end at
the same individual and such that $p_{1}$ starts with an $r$-edge while
$p_{2}$ starts with an $s$-edge.

In fact, the existence of such paths and the connectedness of $\mathcal{A}$
implies $\mathcal{A},\mathcal{O}_{n}\models D(a_{0})$, thus
$\mathcal{A},\mathcal{O}_{n}\models L_{0}(a_{0})$.

We now sketch the construction of a model $\mathcal{I}$ of $\mathcal{A}$ and
$\mathcal{O}_{n}$. Let $\mathcal{W}\subseteq\\{0,\dots,n\\}$ contain $i$ iff
$\mathcal{A}$ contains an assertion $W^{\sigma}_{i}(a)$ for some
$\sigma\in\\{r,s\\}$ and $a\in\mathsf{ind}(\mathcal{A})$. The following
interpretations are used as building blocks for $\mathcal{I}$:

  * •

an _$L_{i}$ -path_, $n\leq i\leq 2n$, is an $r$-path of length $2n-i$ that
makes makes $L_{i+j}$ true at the node at distance $j\in\\{0,\dots,n-i\\}$
from the start of the path and that makes true $A$ at the end of the path;

  * •

a _$K_{i}$ -path_, $n\leq i\leq 2n$, is defined as follows; let $\ell$ be
maximal such that $\\{i-n,\dots,\ell\\}\subseteq\mathcal{W}$; then a
$K_{i}$-path is an $r$-path of length $\ell-(i-n)$ that makes $K_{i+j}$ true
at the node at distance $j\in\\{0,\dots,\ell\\}$ from the start of the path
and that makes true $A$ at the node at distance $2n-i$ (if it exists); in
addition, the start of the path might make true any of the concept names
$V^{\sigma}_{j}$, $\sigma\in\\{r,s\\}$ and $1\leq j\leq n$, which are then all
also made true by all other nodes on the path;

  * •

an _$L_{i}$ -tree_, $1\leq i<n$, is a binary $r/s$-tree of depth $n-i$ that
makes $L_{i+j}$ true at every node on level $j\in\\{0,\dots,n-i\\}$; in
addition, every node on level $n-i$ is the start of an $L_{n}$-path;

  * •

a _$K_{i}$ -tree_, $1\leq i<n$, is a binary $r/s$-tree of depth $n-i$ that
makes true $K_{i+j}$ at every node on level $j\in\\{0,\dots,n-1\\}$ and
$V^{\sigma}_{i+j}$ at every node on level at least $j$ that is a
$\sigma$-successor of its parent; in addition, every node on level $n-i$ is
the start of a $K_{0}$-path; moreover, the root might make true any of the
concept names $V^{\sigma}_{j}$, $\sigma\in\\{r,s\\}$ and $1\leq j\leq i$,
which are then all also made true by all other nodes in the tree.

In all of the above, any node that has an incoming $r/s$-path of length
$i\in\\{1,\dots,2n\\}$ that starts with $\sigma\in\\{r,s\\}$ is additionally
labeled with concept name $U^{\sigma}_{i}$. Moreover, the beginning of the
path/root of the tree may be labeled with concept names of the form
$U^{\sigma}_{i}$. Then any node on depth $i+j$, with $i+j\leq 2n$, is labeled
with $U^{\sigma}_{i+j}$.

Now, the announced model $\mathcal{I}$ is constructed by starting with
$\mathcal{A}$ and doing the following:

  1. 1.

exhaustively apply all concept inclusions in $\mathcal{O}_{n}$ that have a
concept name on the right-hand side;

  2. 2.

at every $a\in\mathsf{ind}(\mathcal{A})$, attach an infinite tree in which
every node has two successors, one for each role name $r,s$, and in which no
concept names are made true;

  3. 3.

if $a\in L_{i}^{\mathcal{I}}$, $0\leq i<n$, then attach at $a$ an
$L_{i}$-tree;

  4. 4.

if $a\in K_{i}^{\mathcal{I}}$, $0\leq i<n$, then attach at $a$ a $K_{i}$-tree;

  5. 5.

if $a\in L_{i}^{\mathcal{I}}$, $n\leq i\leq 2n$, then attach at $a$ an
$L_{i}$-path;

  6. 6.

if $a\in K_{i}^{\mathcal{I}}$, $n\leq i\leq 2n$, then attach at $a$ a
$K_{i}$-path;

  7. 7.

if $W^{\sigma}_{i}(a)\in\mathcal{A}$ for some $a$, then make $W^{\sigma}_{i}$
true everywhere in $\mathcal{I}$.

By going over the concept inclusions in $\mathcal{O}_{n}$ and using Properties
(a) and (b), it can be verified that $\mathcal{I}$ is indeed a model of
$\mathcal{O}_{n}$. In particular, the inclusions $W^{r}_{i}\sqcap
W^{s}_{i}\sqsubseteq L_{0}$ are satisfied since there is no
$d\in\Delta^{\mathcal{I}}$ with $d\in(W^{r}_{i}\sqcap W^{s}_{i})$; if there
was such a $d$, then by construction of $\mathcal{I}$ there are assertions
$W^{r}_{i}(a)$ and $W^{s}_{i}(b)$ in $\mathcal{A}$, in contradiction to the
connectedness of $\mathcal{A}$ and $\mathcal{A},\mathcal{O}_{n}\not\models
L_{0}(a_{0})$. For the CIs $U^{r}_{i}\sqcap U^{s}_{i}\sqsubseteq L_{0}$, we
argue that there is no $d\in\Delta^{\mathcal{I}}$ with $d\in(U^{r}_{i}\sqcap
U^{s}_{i})^{\mathcal{I}}$. To see this, note that there are no
$U^{r}_{i}(a),U^{s}_{i}(a)\in\mathcal{A}$ for any $a$ as otherwise
$\mathcal{A},\mathcal{O}_{n}\models L_{0}(a_{0})$. Now consider Step 1 of the
construction of $\mathcal{I}$ and assume that it adds some
$a\in\mathsf{ind}(\mathcal{A})$ to $(U^{r}_{i}\sqcap
U^{s}_{i})^{\mathcal{I}}$. But this means that
$\mathcal{A},\mathcal{O}_{n}\models U^{r}_{i}(a)$ and
$\mathcal{A},\mathcal{O}_{n}\models U^{s}_{i}(a)$, in contradiction to
$\mathcal{A},\mathcal{O}_{n}\not\models L_{0}(a_{0})$, due to connectedness of
$\mathcal{A}$. Given that there is no $d\in(U^{r}_{i}\sqcap
U^{s}_{i})^{\mathcal{I}}$ for any $i$ after Step 1, it is readily checked that
the elements $d$ added in Steps 2-6 also satisfy $d\notin(U^{r}_{i}\sqcap
U^{s}_{i})^{\mathcal{I}}$.

We now use $\mathcal{I}$ to prove the claim. Let $\mathcal{H}^{\prime}$ be the
set of all $H\in\mathcal{H}_{n}$ with $\mathcal{A},\mathcal{O}_{n}\models
H(a_{0})$. With each $H\in\mathcal{H}^{\prime}$, we associate an
$a_{H}\in\mathsf{ind}(\mathcal{A})$ as follows. Let
$H=\exists\sigma_{1}\cdots\sigma_{2n}.A$. Then $\mathcal{I}$ contains a path
from $a_{0}$ to some element $d_{H}\in A^{\mathcal{I}}$ that is labeled
$\sigma_{1}\cdots\sigma_{2n}$. If $d_{H}\in\mathsf{ind}(\mathcal{A})$, then
$a_{H}=d_{H}$. Otherwise, $d_{H}$ is in a path or tree attached to some
$a\in\mathsf{ind}(\mathcal{A})$. Set $a_{H}=a$. To show that
$||\mathcal{A}||\geq|\\{H\in\mathcal{H}_{n}\mid\mathcal{A},\mathcal{O}_{n}\models
H(a_{0})\\}|$ as required, it suffices to prove that $a_{H}\neq
a_{H^{\prime}}$ whenever $H\neq H^{\prime}$. Thus let
$H,H^{\prime}\in\mathcal{H}^{\prime}$ with $H\neq H^{\prime}$,
$H=\exists\sigma_{1}\cdots\sigma_{2n}.A$, and
$H^{\prime}=\exists\sigma^{\prime}_{1}\cdots\sigma^{\prime}_{2n}.A$. Assume to
the contrary of what is to be shown that $a_{H}=a_{H^{\prime}}$. We
distinguish four cases:

  * •

$d_{H}=a_{H}$, $d_{H^{\prime}}=a_{H^{\prime}}$.

Then there is a path from $a_{0}$ to $a_{H}$ in $\mathcal{I}$ labeled
$\sigma_{1}\cdots\sigma_{2n}$ and a path from $a_{0}$ to $a^{\prime}_{H}$
labeled $\sigma^{\prime}_{1}\cdots\sigma^{\prime}_{2n}$. By construction of
$\mathcal{I}$, these paths must already exist in $\mathcal{A}$. From $H\neq
H^{\prime}$, we thus obtain a contradiction to (e).

  * •

$d_{H}=a_{H}$, $d_{H^{\prime}}\neq a_{H^{\prime}}$.

By construction of $\mathcal{I}$, $d_{H^{\prime}}\neq a_{H^{\prime}}$ implies
that $\mathcal{A},\mathcal{O}_{n}\models L_{i}(a_{H})$ or
$\mathcal{A},\mathcal{O}_{n}\models K_{i}(a_{H})$ for some $i$ with $0\leq
i<2n$. Moreover, $d_{H}=a_{H}$ implies $\mathcal{A},\mathcal{O}_{n}\models
A(a_{H})$. Thus $\mathcal{A},\mathcal{O}_{n}\models D(a_{H})$. By the
connectedness of $\mathcal{A}$, we obtain $\mathcal{A},\mathcal{O}_{n}\models
D(a_{0})$, thus $\mathcal{A},\mathcal{O}_{n}\models L_{0}(a_{0})$ in
contradiction to (c).

  * •

$d_{H}\neq a_{H}$, $d_{H^{\prime}}=a_{H^{\prime}}$.

Symmetric to previous case.

  * •

$d_{H}\neq a_{H}$, $d_{H^{\prime}}\neq a_{H^{\prime}}$.

We first show that $d_{H}$ and $d_{H^{\prime}}$ are not in an $L_{i}$-tree,
$0\leq i<n$. Assume to the contrary that $d_{H}$ is (the case of
$d_{H^{\prime}}$ is symmetric). Then it occurs on level $2n-i$ in the tree,
since $d_{H}\in A^{\mathcal{I}}$. Since an $L_{i}$-tree was attached to
$a_{H}$, we must have $\mathcal{A},\mathcal{O}_{n}\models L_{i}(a_{H})$.
Moreover, there is an $r/s$-path in $\mathcal{I}$ from $a_{0}$ to $a_{H}$ of
length $i$, the prefix of $\sigma_{1}\cdots\sigma_{2n}$ of this length. By
construction of $\mathcal{I}$, this path must already be in $\mathcal{A}$.
This is in contradiction to (c).

We next show that $d_{H}$ and $d_{H^{\prime}}$ are not in a $K_{i}$-tree,
$0\leq i<n$. Assume to the contrary that $d_{H}$ is (the case of
$d_{H^{\prime}}$ is symmetric). Then it occurs on level $2n-i$ in the tree,
since $d_{H}\in A^{\mathcal{I}}$. By definition of such trees (and the
attached paths), this implies that $\mathcal{W}=\\{1,\dots,n\\}$ and thus
$\mathcal{A}$ contains assertions
$W^{\sigma^{\prime\prime}_{1}}_{1}(a_{1}),\dots,W^{\sigma^{\prime\prime}_{n}}_{n}(a_{n})$.
We must further have $\mathcal{A},\mathcal{O}_{n}\models K_{i}(a_{H})$ and
there is an $r/s$-path in $\mathcal{I}$, thus in $\mathcal{A}$ from $a_{0}$ to
$a_{H}$ of length $i$. This is in contradiction to (d).

Thus, $d_{H}$ and $d_{H}^{\prime}$ are both in an $L_{i}$-path or in a
$K_{i}$-path, $n\leq i\leq 2n$. If they are in different such paths, then
$\mathcal{A},\mathcal{O}_{n}\models D(a_{H})$, which is in contradiction to
(c) as $\mathcal{A}$ is connected. Thus, they must be in the same $L_{i}$-path
or in the same $K_{i}$-path. Since each such path contains a single element
$d$ with $d\in A^{\mathcal{I}}$, we obtain $d_{H}=d^{\prime}_{H}$. From $H\neq
H^{\prime}$, it thus follows that there are two different paths of length $i$
in $\mathcal{I}$ from $a_{0}$ to $a_{H}$, the prefixes of this length of
$\sigma_{1}\cdots\sigma_{2n}$ and of
$\sigma^{\prime}_{1}\cdots\sigma^{\prime}_{2n}$. This is in contradiction to
(e).

This finishes the proof of the claim.

We can use the claim to show the following invariant:

  * ($*$)

at any point in time, the sum $m$ of the sizes of the inputs to membership and
equivalence queries made so far is not smaller than the number of candidates
that were removed from $\mathcal{H}$.

Note in fact that only Cases 2 and 3 of membership queries and Cases 3 and 6
of equivalence queries may remove candidates from $\mathcal{H}$ and that they
all remove only one candidate for each query posed with the exception of Case
3 of membership queries which can remove multiple candidate. However, the
claim implies that the number of removed candidates in Case 3 of membership
queries is bounded from above by the size of the query posed.

It is clear that there is a polynomial $q_{3}$ such that the size of all
counterexamples returned by the oracle is at most $q_{3}(n)$. The overall sum
of the sizes of posed membership and equivalence queries is bounded by
$p(q_{1}(n),q_{2}(n),q_{3}(n))$. It thus follows from ($*$) that at most
$p(q_{1}(n),q_{2}(n),q_{3}(n))$ candidate concepts have been removed from
$\mathcal{H}_{n}$. By the choice of $n$, at least two candidate concepts
remain in $\mathcal{H}$ after the algorithm finished. Thus, the learner cannot
distinguish between them, and we have derived a contradiction. ∎