models of of finite -outdegree as input to the tree automata.
Since 2ATAs run over binary trees, we need to appropriately encode the
arbitrary outdegree, which is done similar to [25].

More precisely, we use the alphabet $\Theta$ defined by

\[\Theta = \{\circ\}\cup \text{Rol}(\Kmc)\times
2^{\text{ind}(\Dmc)\cup (\text{sig}(\Kmc)\cap \mn{N_C})}\times

where $\text{Rol}(\Kmc)$ denotes the set of all role names that occur
in and their inverses, and $\Fmc$ is the set of all pairs $(r,a)$
with $r$ a role name that in $\text{sig}(\Kmc)$ and $a\in
\text{ind}(\Dmc)$.  Intuitively, a node $w\in T$ with
$\tau(w)=(R,M,F)$ encodes an element that satisfies precisely the
concepts in $M$; moreover, $F$ describes its connections to
elements in $\text{ind}(\Dmc)$ and $R$ is the “incoming role”.
The symbol `$\circ$' is a label for dummy nodes that
we need for encoding arbitrary finite outdegree into binary trees: we simply
introduce as many intermediate $\circ$-labeled nodes as needed to
achieve the required outdegree at each node.

More formally, let $(T,\tau)$ be a $\Theta$-labeled tree.
For each $w \in T$ with
$\tau(w) \neq \circ$, let $w^\uparrow$ denote the unique ancestor $w'$
of $w$ in $T$
(if existing) such that $\tau(w') \neq
\circ$ and $\tau(w'')=\circ$ for all $w''$ between $w'$ and $w$.
We call $(T,\tau)$ well-formed if

* for every
$a\in\text{ind}(\Dmc)$, there is a unique element $w_{a}
\in T$ such that $\tau(w_a)=(R,M,F)$ for some $R,F$ and $a\in M$;

* for every $w\in T$ with $\tau(w)\neq \circ$, either $w=w_a$,
for some $a$, and all ancestors of $w$ are labeled with $\circ$,
or $w$ has an ancestor $w_a$, for some $a$.

A well-formed $\Theta$-labeled tree $(T,\tau)$ gives rise to a
structure $\Amf_\tau$ with $\text{dom}(\Amf_\tau) = \{ w \in T
\mid \tau(w)\neq \circ\}$ as follows:

$$ \begin{array}{r@{\;}c@{\;}l}
a^{\Amf_\tau} &=& w_{a} \\[1mm]
A^{\Amf_\tau} &=& \{ w\in T \mid \tau(w)=(S,M,F) \text{ and } A \in
M \} \\[1mm]
r^{\Amf_\tau} &=& \{ (w^\uparrow,w) \mid
\tau(w)=(r,M,F)\text{ and }
w^\uparrow\text{ defined}\} \cup{} \\[1mm]
&& \{ (w,w^\uparrow) \mid \tau(w)=(r^-,M,F)\text{ and }w^\uparrow\text{ defined}\} \cup{} \\[1mm]
&& \{ (w,w_a) \mid \tau(w)=(S,M,F)\text{ and } (r,a)\in
F\} %\cup{} \\[1mm]
%     && \{ (w_a,w) \mid \tau(w)=(S,M,F)\text{ and } (R^-,a)\in F\}
\end{array} $$

for all $a \in \mn{N_I}$, $A \in \mn{N_C}$, and $r \in \mn{N_R}$ (and
for $a\in\mn{N_I}\setminus \text{ind}(\Dmc)$, $w_a$ denotes an
arbitrary element of $\Amf$).

Conversely, every finite outdegree forest model of can be encoded
(up to isomorphism) as well-formed $\Theta$-labeled tree.
To show this, we
start with a not-necessarily binary well-formed $\Theta$-labeled tree
$(T,\tau)$ that encodes $\Amf$; $(T,\tau)$ can easily be made binary
by introducing intermediate $\circ$-labeled nodes. Let $D=\{a^\Amf\mid
a\in \text{ind}(\Dmc)\}$ and associate sets $M_d,F_d$ to every
element $d\in \text{dom}(\Amf)$ by taking

$$ \begin{array}{r@{\;}c@{\;}l}
M_d &=& \{A\in\text{sig}(\Kmc)\mid d\in A^\Amf\}\cup \{a\in
\text{ind}(\Dmc) \mid d=a^\Amf\} \\[1mm]
F_d &=& \{(r,e)\mid (d,e)\in r^\Amf, e\in D\}
\end{array}$$

To start the construction of $(T,\tau)$, we set $\tau(\varepsilon)=\circ$ and
add a successor $w_d$ of $\varepsilon$ for every $d\in D$ and label it
with $\tau(w_d)=(S,M_d,F_d)$ for an arbitrary role name $S$.

For the rest of the construction, let $\Amf_d,d\in D$ be the -trees
which exist since $\Amf$ is -forest model of .  Recall that
$\Amf_d$ is rooted at $d$. Now $(T,\tau)$ is obtained by exhaustively applying the
following rule:

$(\ast)$ If $w_e$ is defined, for an
element $e$ of some $\Amf_d$ and $f$ is a successor of $e$ in $\Amf_d$
with $w_f$ undefined, add a fresh successor $w_f$ of $w_e$ to $T$ and
set $\tau(w_f)=(R,M_f,F_f)$ where $R$ is the unique role such
that $(e,f)\in R^\Amf$.

It is not difficult to construct 2ATAs that accept precisely the
forest models of , see for
example [22] for full details of a
similar automata construction.

For $\Lmc\in\{\ALC,\ALCI,\ALCO\}$ and -KBs ,
we can construct in time polynomial in $||\Kmc||$
2ATAs $\Amc_0,\Amc_\Kmc$ such that:

* $\Amc_0$ accepts precisely the well-formed $\Theta$-labeled

* $\Amc_\Kmc$ accepts a well-formed $\Theta$-labeled tree
$(T,\tau)$ iff $\Amf_\tau$ is a finite outdegree forest model of

§.§ and

We concentrate on , the case of is similar.

“if”. Take a forest model $\Amf$ and some $a\in P$ with $\Dmc_{\text{con}(a)},a
\rightarrow^{\Sigma}_{c} \Amf,b^{\Amf}$.
Moreover, fix a $\Sigma$-homomorphism $h$ and
-types $t_{d}$, $d\in
\text{ind}(\Dmc)$ that witness that.
Take models $\Bmf_{d}$ of $\Omc$ such that
$\Bmf_{d},d \sim_{\ALCI,\Sigma} \Amf,h(d)$. We may assume that the
$\Bmf_{d}$ are tree-shaped with root $d$ and that the bisimulations
are functions $f_{d}$.  Now attach to every $d\in \text{ind}(\Dmc)$
the model $\Bmf_{d}$ and obtain $\Bmf$ by adding $(d,d')$ to
$r^{\Bmf}$ if $r(d,d')\in \Dmc$. Then
\[f= \bigcup_{d\in
\text{ind}(\Dmc)}f_{d}\]
is a functional
$\ALCI(\Sigma)$-bisimulation between $\Bmf$ and $\Amf$.

“only if”. Take a forest model $\Amf$, some $a\in P$, and a model
$\Bmf$ of such that $\Bmf,a^{\Bmf}\sim_{\ALCI,\Sigma}^{f}
\Amf,b^{\Amf}$.  Let $f$ be a functional
$\ALCI(\Sigma)$-bisimulation witnessing that. The restriction
$h$ of $f$ to $\text{ind}(\Dmc)$ and types $t_d=\text{tp}_\Kmc(\Bmf,d^\Bmf)$,
for all $d\in\text{ind}(\Dmc)$ witness $\Dmc_{\text{con}(a)},a
\rightarrow^{\Sigma}_{c} \Amf,b^{\Amf}$.

Let $\Lmc\in\{\ALC,\ALCI\}$.  For each $a\in P$, there is a 2ATA
$\Amc_a$ such that $\Amc_a$ accepts a well-formed labeled tree
$(T,\tau)$ iff $\Dmc_{\text{con}(a)},a \rightarrow^{\Sigma}_{c}
\Amf,b^{\Amf}$.  Moreover, $\Amc_a$ can be constructed in double
exponential time in $||\Kmc||$ and has exponentially many states.

We sketch the construction of the automata $\Amc_a$, $a\in P$. Let
$(T,\tau)$ be a well-formed input tree.
As the first step, $\Amc_a$ non-deterministically guesses the following:

* types $t_d$, $d\in\text{ind}(\Dmc_{\text{con}(a)})$, such
that $(\Omc,\Dmc')$ is satisfiable where  $\Dmc'=\Dmc\cup \{
C(d) \mid C \in t_d, \ d\in
\text{ind}(\Dmc_{\text{con}(a)})\}$;

* a partition $\Dmc_0,\Dmc_1,\ldots,\Dmc_m$ of
$\Dmc_{\text{con}(a)}$ such that
$\text{ind}(\Dmc_i)\cap\text{ind}(\Dmc_j) = \emptyset$ for
$1\leq i<j\leq m$;

* a mapping $h$ from $\text{ind}(\Dmc_0)$ to
$\text{ind}(\Dmc)$ such that $h(a)=b$ and there are
$a_1,\dots,a_m$ with $h(c)=a_i$
for all $c \in \text{ind}(\Dmc_0 \cap \Dmc_i)$ and
$1 \leq i \leq m$.

The entire guess is stored in the state of the automaton. Note that
the first item above ensures that Item (ii) from the definition of
$\Dmc_{\text{con}(a)},a \rightarrow^{\Sigma}_{c}
\Amf_\tau,b^{\Amf_\tau}$ is satisfied for the guessed types
$t_d$. Moreover, elements $d^\Bmf$ for $d\in\text{ind}(\Dmc_0)$ are intuitively mapped to
$h(d)^\Amf$ while elements $d^\Bmf$ for
$d\in\text{ind}(\Dmc_i)\setminus\text{ind}(\Dmc_0)$ are mapped to
the trees below $a_i$.

After making its guess, the automaton verifies first $h$ is a
$\Sigma$-homomorphism from $\Dmc_0$ to $\Amf_\tau$ by sending out
copies for all facts in $\Dmc_0$ to the respective elements in
$\Amf_\tau$. Then, it verifies that  this homomorphism can be
extended to a homomorphism from $\Dmc_{\text{con}(a)}$ to
$\Amf_\tau$ that satisfies Item (i) from the definition of
$\Dmc_{\text{con}(a)},a \rightarrow^{\Sigma}_{c}
\Amf_\tau,b^{\Amf_\tau}$. To this end, it does a top-down traversal
of $\Amf_\tau$ checking that each $\Dmc_i$ can be homomorphically
mapped to the subtree of $\Amf_\tau$ below $h(a_i)^{\Amf_\tau}$. During the
traversal, the automaton memorizes in its state the set of
individuals from $\Dmc_i$ that are mapped to the currently visited

The automaton additionally makes sure that Item (i) from the definition
$\Dmc_{\text{con}(a)},a \rightarrow^{\Sigma}_{c}
\Amf_\tau,b^{\Amf_\tau}$ is satisfied, in the following way. During
the top-down traversal, it spawns copies of itself to verify that,
whenever it has decided to map a
$d \in \text{ind}(\Dmc_{\text{con}(a)})$ to the current element, then
there is a tree-shaped model $\Bmc_d$ of with
$\text{tp}_{\Kmc}(\Bmf_{d},d) = t_{d}$ and a bisimulation that
witnesses $\Bmc_d,d \sim_{\ALCI,\Sigma} \Amf_\tau,c$. This is done by
`virtually' traversing $\Bmc_d$ elements-by-element, storing at each
moment only the type of the current element in a state. This is
possible because $\Bmf_d$ is tree-shaped. At the beginning, the
automaton is at an element of $\Bmc_d$ of type $t_d$ and knows that
the bisimulation maps this element to the node of $\Amf_\tau$
currently visited by the automaton. It then does two things to verify
the two main conditions of bisimulations.  First, it transitions to
every neighbor of the node of $\Amf_\tau$ currently visited, both
upwards and downwards, and carries out in its state the corresponding
transition in $\Bmc_d$, in effect guessing a new type. Second, it
considers the current type of $\Bmc_d$ and guesses successor types
that satisfy the existential restrictions in it. For every required
successor type,  it then guesses a neighbor of the currently visited
node in $\Amf_\tau$ to which the successor is mapped. The two steps
are alternated, exploiting the alternation capabilities of the
automaton. Some extra bookkeeping in states is needed for the root
node of the input tree as it represents more than one element
of $\Amf_\tau$.

It can be verified that only exponentially many states are required
and that the transition function can be computed in double exponential
time in $||\Kmc||$.

We can now finish the proof of the upper bound in
Theorem <ref>. By
Lemmas <ref>, <ref>,
and <ref> and Theorem <ref>,
$(\Kmc,P,\{b\})$ is projectively $\Lmc(\Sigma)$-separable iff

\[L(\Amc_0)\cap L(\Amc_\Kmc)\cap \textstyle\bigcap_{a\in
where $\overline{L(\Amc_a)}$
denotes the complement of $L(\Amc_a)$. By Lemmas <ref>
and <ref> all these automata can be constructed in
double exponential time and their number of states is single
exponential in $||\Kmc||$ for $\Lmc\in\{\ALC,\ALCI\}$.  By
Lemma <ref>, we can compute in polynomial time
an automaton that accepts precisely the language on the left-hand side
of the above inequality. It remains to recall that non-emptiness of
2ATAs can be decided in time exponential in the number of states.

§.§ Upper Bound for

We give here only the upper bound for
Theorem <ref>. The lower bound is proved for
conservative extensions in Section <ref>.

We use the same definition of -types as in
except that we assume without loss of generality that $\{c\}\in
\text{sub}(\Kmc)$, for all $c\in\text{ind}(\Dmc)$. Denote with
$\text{TP}(\Kmc)$ the set of all types.

We work with $(\Theta\times\Theta')$-labeled trees for

\[\Theta' = \{\circ\} \cup 2^{\text{ind}(\Dmc)}\]

A $(\Theta\times\Theta')$-labeled tree $(T,\tau_1,\tau_2)$ is
well-formed if $(T,\tau_1)$ is well-formed and for each
$c\in\text{ind}(\Dmc)$, there is exactly one $w\in T$ with $c\in
\tau_2(w)$; we denote this with $v_c$.

There is a 2ATA $\Amc_0'$ which accepts precisely the well-formed
$(\Theta\times\Theta')$-labeled trees.

For every $a\in P$, there is a 2ATA $\Amc_a'$ which accepts a
well-formed $(\Theta\times\Theta')$-labeled tree $(T,\tau_1,\tau_2)$
iff there is a forest model $\Bmf$ of and a
function $f:\text{dom}(\Bmf)\to \text{dom}(\Amf_{\tau_1})$ such that

* $f$ witnesses $\Bmf,a^\Bmf\sim_{\ALCO,\Sigma}^f
\Amf_{\tau_1},b^{\Amf_{\tau_1}}$;

* for every $c\in \text{ind}(\Dmc)$, we have $f(c^\Bmf)=v_c$.

Moreover, $\Amc_a'$ can be
constructed in exponential time in $||\Kmc||$ and has at most
exponentially many states.

Let $(T,\tau_1,\tau_2)$ be a well-formed
$(\Theta\times\Theta')$-labeled tree. We sketch the function of
$\Amc'_a$. Intuitively, $\Amc_a'$ constructs an -forest model
of and the witnessing bisimulation $f$ “on the fly” by
visiting the nodes in the input in states that store the type of the
currently visited element of . The construction of is
started at the individual names, that is, at the nodes $v_c\in T$,
$c\in \text{ind}(\Dmc)$.  Before the actual construction of can
start, $\Amc_a'$ guesses the types of the individual names $c\in
\text{ind}(\Dmc)$ in the model $\Bmf$ and keeps that guess in its
state throughout the entire run. Then it spawns a copy of itself in
every $v_c\in T$, $c\in\text{ind}(\Dmc)$ in state corresponding to

Whenever $\Amc_a'$ visits a node $w\in T$ in some type $t$, this
represents an obligation to extend the bisimulation constructed so
far to an element $e$ of type $t$ in and the element $w$ of
$\Amf_{\tau_1}$. This can be done similarly to what is done in the
proof of Lemma <ref> since $\Bmf$ is
forest-shaped. We need to argue, however, how to deal with the
individuals since they can be accessed from everywhere in . When
the automaton tries to extend with a successor that satisfies
some nominal $\{c\}$, we have to make sure that that successor gets
type $t_c$. Conversely, when we try to find a type bisimilar to some
successor of $w$, we make sure that we can only visit nodes of the
form $v_c$ with types $t_c$. In both cases, it is crucial that the
automaton can stop the extension, because we have already started a
copy of the automaton with type $t_c$ in $v_c$ (in the very

We finish the proof of the upper bound of
Theorem <ref>. By
Lemma <ref>, we can compute in exponential time
(in the size of $\Amc_{a}'$)  an automaton $\Amc_a$ with

\[L(\Amc_a) = \{(T,\tau_1)\mid (T,\tau_1,\tau_2)\in L(\Amc_a')\},\]

that is, $\Amc_a$ is the projection of $\Amc_a'$ to the first
component $\tau_1$. It should be clear that $\Amc_a$ accepts a forest
model of iff there is a model $\Bmf$ of such that
$\Bmf,a^{\Bmf}\sim^f_{\ALCO,\Sigma}\Amf,b^{\Amf}$. Thus, we can
proceed as for and compute the desired automaton $\Amc$ such
that it accepts the language

\[L(\Amc)=L(\Amc_0)\cap L(\Amc_\Kmc)\cap \textstyle\bigcap_{a\in

which is non-empty iff $(\Kmc,P,\{b\})$ is projectively
$\ALCO(\Sigma)$-satisfiable. Since $\Amc_a$ (and thus ) is a 2ATA
with double exponential many states and non-emptiness can be checked
in exponential time in the number of states, the -upper
bound follows.

§ LOWER BOUND FOR CONSERVATIVE EXTENSIONS IN

We start with model theoretic characterizatons of conservative
extensions and projective conservative extensions in .  We define
a model $\Amf$ of an $\ALCO$-ontology $\Omc$ to be a forest
model of $\Omc$ of finite outdegree if it is an $\ALCO$-forest
model of the KB $\Kmc=(\Omc,\Dmc)$ of finite $\ALCO$-outdegree, where
$\Dmc= \{D_{b}(b) \mid b\in \text{ind}(\Omc)\}$ and the $D_{b}$ are
fresh concept names, one for each individual $b$ in $\Omc$.

Let $\Omc$ and $\Omc'$ be $\ALCO$-ontologies and $\Sigma
= \text{sig}(\Omc)$. Then

* the following conditions are equivalent:

* $\Omc \cup \Omc'$ is a conservative extension
of $\Omc$;

* for every pointed forest model $\Amf,a$ of $\Omc$ of finite outdegree there exists a pointed model $\Bmf,b$ of $\Omc\cup \Omc'$ such that
$\Bmf,b \sim_{\ALCO,\Sigma} \Amf,a$.

* the following conditions are equivalent:

* $\Omc \cup \Omc'$ is a projective conservative extension of $\Omc$;

* for every pointed forest model $\Amf,a$ of $\Omc$ of finite outdegree there exists a pointed model $\Bmf,b$ of $\Omc\cup \Omc'$ such that
$\Bmf,b \sim_{\ALCO,\Sigma}^{f} \Amf,a$.

Given an -ontology $\Omc$ and an -ontology $\Omc'$, it is
-hard to decide whether $\Omc'$ is a conservative
extension of $\Omc$.

Since is an -ontology, we have no nominals available in
witness concepts and every witness concept must actually be an -concept.

It is
interesting to note that we use only a single nominal in the
ontologies $\Omc'$.

The proof of Theorem <ref> follows the general
outline of the lower bound for conservative
extensions in that is proved in [12].

As in that paper, we proceed in two steps. We first establish a lower
bound on the size of witness concepts and then extend the involved
ontologies to obtain the lower bound.  In fact, the
step is the technically subtle one and we present it in full detail.
The second step is then rather simple and we only sketch the required

§.§ Large Witness Concepts

For every $n > 0$, there is an -ontology $\Omc_n$ and an
-ontology $\Omc'_n$ such that the size of $\Omc_n$ and
$\Omc'_n$ is polynomial in $n$, $\Omc_n \cup \Omc'_n$ is not a
conservative extension of $\Omc_n$, and every witness concept $C$
for $\Omc_n$ and $\Omc'_n$ is of size at least $2^{2^{2^{2^n}}}$.

To prove Theorem <ref>, we craft $\Omc_n$ and $\Omc'_n$
so that $\Omc_n \cup \Omc'_n$ is not a conservative extensions of
$\Omc_n$, but every witness concept $C$ for $\Omc_n$ and $\Omc'_n$
must enforce in models of $\Omc_n$ a binary tree of depth at least
$2^{2^{2^n}}$.  This implies that $C$ is of size at least $2^m$
because $C$ is an -concept and $\Omc_n$ does not introduce
additional elements via existential restrictions. Let us be a bit more
precise about the trees. The `nodes' of the tree are actually paths of
length $2^n \cdot 2^{2^n}$ and no branching occurs inside these
paths. Thus, when counting also the intermediate domain element
on the `node paths', then the trees are really of depth
$2^n \cdot 2^{2^n} \cdot 2^{2^{2^n}}$.  We use a single role name
$r$ to attach successors, both when branching occurs and when no
branching occurs. At branching nodes, the left successor is marked
with concept name $S_L$ and the right successor is marked with concept
name $S_R$. Successors of non-branching nodes must be marked with at
least one of $S_L$ and $S_R$. And finally, the (first element of the)
root (path) is labeled with concept name $A$.

A main feature of $\Omc_n$ and $\Omc'_n$ is to implement a binary
counter that can count up to $m:=2^{2^{2^n}}$, the desired depth of the
trees (not counting intermediate domain elements). In fact, $\Omc_n$
and $\Omc'_n$ implement three binary counters that build upon each
other so that the third counter can achieve the intended counting
range.  Counter 1 has $n$ bits and counts from $0$ to $2^n-1$,
Counter 2 has $2^n$ bits and counts up to ${2^{2^n}}-1$, and Counter 3
has $2^{2^n}$ bits and counts up to ${2^{2^{2^n}}}-1$. We use
Counter 1 to describe the bit positions of Counter 2 and Counter 2 to
describe the bit positions of Counter 3.  Counter 1 and Counter 2
count modulo their maximum value plus one while Counter 3 needs to
reach its maximum value only once.

Counter 1 uses concept names $C_0,\dots,C_{n-1}$ as bits.  Thus a
counter value of Counter 1 can be represented at a single domain
element. In contrast, a value of Counter 2 is spread out accross a
sequence of $2^n$ domain elements, which we call a Counter 2
sequence. The bit positions of Counter 2 in such a sequence are
identified by Counter 1 and concept name $X_2$ is used to indicate the
bit value of Counter 2 at each position. A value of Counter 3, in
turn, is spread out accross a sequence of $2^{2^n}$ Counter 2
sequences, that is, $2^n \cdot 2^{2^n}$ domain
elements in total. We call this a Counter 3 sequence and
it is these Counter 3 sequences that constitute the `nodes' of
the trees mentioned above. Each of
the Counter 2 subsequences represents one bit position of Counter 3 and stores
one bit value via the concept name $X_3$ that must be
interpreted uniformly in that subsequence.

With a path in an structure , we mean a sequence
$p=d_0,\dots,d_n$ of elements of $\text{dom}(\Amf)$ such that
$(d_i,d_{i+1}) \in r^\Amf$ and $d_{i+1} \in S_L^\Amf \cup S_R^\Amf$
for all $i < n$. We say that such a path is properly counting
if the concept names $C_0,\dots,C_{n-1},X_2,X_3$ are interpreted along
the path in accordance with the counting strategy outlined above, all
three counters starting with counter value zero. We now formalize the
trees described above. A counting tree in is a collection
$T$ of (not necessarily distinct) domain elements $d_{w,i}$,
$w \in \{L,R\}^*$ with $|w|<m$ and
$0 \leq i < 2^n \cdot 2^{2^n}$, such that the following conditions are

* $d_{\varepsilon,0} \in A^\Amf$,

* $(d_{w,i},d_{w,i+1}) \in r^\Amf$ and $d_{w,i+1} \in S_L^\Amf
\cup S_R^\Amf$
for all $d_{w,i+1} \in T$;

* $(d_{w, 2^n \cdot 2^{2^n}},d_{wL,0}) \in r^\Amf$ and $d_{wL,0}
\in S_L^\Amf$
for all ;

* $(d_{w, 2^n \cdot 2^{2^n}},d_{wR,0}) \in r^\Amf$ and $d_{wR,0}
\in S_R^\Amf$
for all ;

* every path in that uses only elements from $T$ is properly

The element $d_{\varepsilon,0}$ is the root of the counting
tree.  We say that is witnessing if there is a $d \in
such that
the following conditions are satisfied:

* $d$ is the root of a counting tree;

* every path that starts at $d$ and is of length at most $m$ is
properly counting.

We are now in a position to describe more concretely what we want to
achieve. Let $m' := 2^n \cdot 2^{2^n} \cdot m$.  For
$0 \leq i \leq m'$, let $S_i$ denote the set of concept names from
$S:=\{C_0,\dots,C_{n-1},X_2,X_3\}$ that the $i$-th domain element on a
path that is properly counting must satisfy. Then set

\begin{array}{rcl}
D_{0} &:=& \top \\ %if $|w| = m-1$ and $i=2^n\cdot2^{2^n}$\\
D_{i+1} &:=& \exists r . (S_L \sqcap D_{i}) \sqcap \exists r . (S_R
\sqcap D_i) \\
C_i &:=& A \sqcap D_i \sqcap \bigsqcap_{0 \leq i \leq m'}
\forall r^i . (\bigsqcap S_i \sqcap \neg \bigsqcup S
\setminus S_i)
\end{array}

Note that every model of $C_m'$ is witnessing.  We craft $\Omc_n$ and
$\Omc'_n$ such that the following holds.

* $C_{m'}$ is a witness concept for $\Omc_n$ and $\Omc'_n$;

* for every pointed model $\Amf,d$ of $\Omc_n$ of finite outdegree
that is not witnessing, there is a pointed model $\Bmf,e$ of
$\Omc_n \cup \Omc'_n$ such that $\Bmf,e \sim^f_{\ALCO,\Sigma}
\Amf,d$ where $\Sigma=\text{sig}(\Omc_n)$.

Point 2 implies that every witness concept for
$\Omc_n$ and $\Omc'_n$ must have size at least $2^m$. In fact,

if an -concept $C$ that is satisfiable w.r.t. $\Omc_n$ does not
mention all paths in a counting tree, including their labeling with
$S_L$ and $S_R$, then there is a model of $C$ and $\Omc_n$ in
which there is no counting tree.  Informally, this is because $\Omc_n$
does not introduce additional elements via existential quantifiers;
for a rigorous proof of an almost identical statement, see
[12]. We argue that such a $C$ cannot be a witness
concept. Let $d \in C^\Amf$.  By Point 2, there is a pointed model
$\Bmf,e$ of $\Omc_n \cup \Omc'_n$ such that
$\Bmf,e \sim^f_{\ALCO,\Sigma} \Amf,d$. Since -concepts are
preserved under -bisimulations, this implies $e \in C^\Bmf$.
Consequently, $C$ is satisfiable w.r.t. $\Omc_n \cup \Omc'_n$ and
is not a witness concept for $\Omc_n$ and $\Omc'_n$.

Now for the actual construction of $\Omc_n$ and $\Omc'_n$.
The ontology $\Omc_n$ is given in Figure <ref>.

\begin{eqnarray}
\top &\sqsubseteq & \forall r. \neg A \\[2mm]
A & \sqsubseteq & (C_1=0) \\
\top &\sqsubseteq& \forall r. (C_1{+}{+}) \\[2mm]
A & \sqsubseteq & F_2 \\
F_2 \sqcap (C_1<2^n) &\sqsubseteq& \forall r . F_2 \\
F_2 &\sqsubseteq& \neg X_2\\[2mm]
(C_1=0) &\sqsubseteq& \neg Z_2 \\
\neg X_2 \sqcap \neg (C_1=2^n-1) &\sqsubseteq& \forall r . Z_2 \\
Z_2 \sqcap \neg (C_1=2^n-1) &\sqsubseteq& \forall r . Z_2 \\
X_2 \sqcap \neg Z_2 \sqcap \neg (C_1=2^n-1)  &\sqsubseteq& \forall r
. \neg
(C_1 < 2^n-1) \sqcap X_3  &\sqsubseteq&  \forall r .X_3 \\
(C_1 < 2^n-1) \sqcap \neg X_3  &\sqsubseteq& \forall r . \neg X_3
\\[2mm]
(C_1=2^n-1) \sqcap \neg Z_2 \sqcap X_2 &\equiv& E_3 \\[2mm]
A &\sqsubseteq& F_3 \\
F_3 \sqcap \neg (C_1=2^n-1) &\sqsubseteq&  \forall r. F_3 \\
F_3 \sqcap (C_1=2^n-1) \sqcap \neg E_3 &\sqsubseteq&  \forall r. F_3 \\
F_3 &\sqsubseteq& \neg X_3 \\[2mm]
% F_3 \sqcap (C_1<2^n-1) & \sqsubseteq&  \forall (r \cup s). F_3 \\
% F_2' \sqcap (C_1=2^n-1) \sqcap Z_2& \sqsubseteq&  \forall (r \cup s). F'_2 \\
% F_2' \sqcap (C_1=2^n-1) \sqcap \neg X_2& \sqsubseteq&  \forall (r \cup
% s). F'_2 \\
%  A \sqcup E&\sqsubseteq& \neg Z_3 \\
% (C_1=2^n-1) \sqcap \neg Z_2 & \sqsubseteq& \forall (r \cup s) .\neg
% Z_3 \\
A & \sqsubseteq & \neg Z_3 \\
E_3 & \sqsubseteq & \forall r . \neg Z_3\\
(C < 2^n-1) \sqcap Z_3 &\sqsubseteq& \forall r . Z_3 \\
(C < 2^n-1) \sqcap \neg Z_3 &\sqsubseteq& \forall r . \neg Z_3 \\
\neg X_3 \sqcap (C = 2^n-1) \sqcap \neg E_3 &\sqsubseteq& \forall r . Z_3 \\
Z_3 \sqcap (C = 2^n-1) \sqcap \neg E_3 &\sqsubseteq& \forall r . Z_3 \\
X_3 \sqcap \neg Z_3 \sqcap (C = 2^n-1) \sqcap \neg E_3 &\sqsubseteq& \forall r .\neg Z_3 \\[2mm]
E_3 &\sqsubseteq& L_2 \\
(C_1 < 2^n-1) \sqcap \exists r . L_2 & \sqsubseteq& L_2 \\[2mm]
E_3 \sqcap \neg Z_3 \sqcap X_3&\sqsubseteq& L_3 \sqcap L'_3\\
(C_1 < 2^n-1) \sqcap \exists r . L'_3 & \sqsubseteq& L_3 \sqcap L'_3\\
(C_1 < 2^n-1) \sqcap \exists r . L_3 & \sqsubseteq& L_3 \\
(C_1 < 2^n-1) \sqcap X_2 \sqcap \exists r . L_3 & \sqsubseteq& L_3
\sqcap
L'_3 \\
(C_1 = 2^n-1) \sqcap \exists r . L'_3 & \sqsubseteq & L_3 \\
(C_1 = 2^n-1) \sqcap X_2 \sqcap \exists r . L'_3 & \sqsubseteq & L_3
\sqcap
\\[2mm]
S_L \sqcup S_R &\sqsubseteq& \top
\end{eqnarray}

The ontology $\Omc_n$.

We use $C \equiv D$ as an abbreviation for $C \sqsubseteq D$ and
$D \sqsubseteq C$. Line (1) makes sure that $A$ cannot be true at
non-root nodes of counting trees, which would enable undesired witness
concepts such as $A \sqcap \exists r^{2^n} . A$.  Lines (2) and (3)
guarantees that Counter 1 starts with value 0 at $A$ and is
incremented modulo $2^n$ when passing to an $r$-child where
$\forall r .  (C_1{+}{+})$ is an abbreviation for a more complex
concept (of size polynomial in $n$) that achieves this; it is standard
to work out details, see e.g. [12].  The concepts
$(C_1=0)$, $(C_1=2^n-1)$, and $(C_1 < 2^n-1)$ are also abbreviations,
with the obvious meaning.  Lines (4) to (6) make sure that Counter 2
starts with value 0 in all paths that are outgoing from an instance of
$A$. Lines (7) to (10) guarantee that concept name $Z_2$ is true at a
domain element in a Counter 2 sequence iff there was a zero bit
strictly earlier in that sequence. Lines (11)-(12) ensure that the
concept name $X_3$ which represents bit values for Counter 3 is
interpreted uniformly in Counter 2 sequences (which represent a single
bit position of Counter 3). Line (13) guarantees that concept name
$E_3$ marks exactly the final domain element on Counter 3 sequences.
Lines (14)-(17) enforce that Counter 3 starts with value 0 in all
paths that are outgoing from an instance of $A$. Lines (18)-(24) make
sure that concept name $Z_3$ is true at a domain element in a
Counter 3 sequence iff there was a zero bit strictly earlier in that
sequence. Lines (25)-(26) gurantee that $L_2$ is true in the last
element of every Counter 2 sequence and Lines (27)-(32) achive that
$L_3$ is true in the last Counter 2 subsequence of every Counter 3
sequence. In both cases, we do not need the converse (altough it would
be possible to achieve also the converse with further concept
inclusions). Note that we do not use the concept names $S_L$ and
$S_R$ as this does not turn out to be necessary. However, we want
them to be part of $\text{sig}(\Omc_1)$, which is achieved by Line (33).

\begin{eqnarray}
A & \sqsubseteq & P_1 \sqcup P_2 \sqcup P_3 \\[2mm]
P_1 \sqcap E_3 \sqcap \neg Z_3
\sqcap X_3 & \sqsubseteq &  \forall r . (S_L \rightarrow P_1)
\sqcup \forall r . (S_R \rightarrow P_1) \\
P_1 \sqcap E_3 \sqcap \neg Z_3
\sqcap X_3 & \sqsubseteq &
\bot \\[2mm]
P_2 &\sqsubseteq& M_0 \sqcup \exists r . ((S_L \sqcup S_R) \sqcap P_2) \\
P_2 & \sqsubseteq& \neg (L_2 \sqcap L_3)\\[2mm]
%  L_2 \sqcap L_3 & \sqsubseteq& \neg P_2 \\[2mm]
M_0 &\sqsubseteq& M \sqcap (D_1=0) \\
M_0 \sqcap \neg Z_2 &\sqsubseteq& NX_2 \leftrightarrow X_2 \\
M_0 \sqcap Z_2 &\sqsubseteq& NX_2 \leftrightarrow \neg X_2 \\
M \sqcap (D_1 < 2^n-1) &\sqsubseteq& \forall r . (D_1{+}{+}) \\
M \sqcap (D_1 < 2^n-1) \sqcap NX_2 &\sqsubseteq& \exists r. ((S_L \sqcup S_R) \sqcap M \sqcap NX_2)\\
M \sqcap (D_1 < 2^n-1) \sqcap \neg NX_2 &\sqsubseteq& \exists
r. ((S_L \sqcup S_R) \sqcap M \sqcap \neg NX_2) \\
M \sqcap (D_1=2^n-1) \sqcap NX_2 &\sqsubseteq& X_2 \\
M \sqcap (D_1=2^n-1) \sqcap \neg NX_2 &\sqsubseteq& \neg X_2 %\\[2mm]
% M \sqcap (D_1<2^n-1) \sqcap (C_1=2^n-1) & \sqsubseteq& Z_2 \sqcup \neg X_2\\
\end{eqnarray}

The first part of ontology $\Omc'_n$.

We present the ontology $\Omc'_n$ in two parts, one
pertaining to Counter 2 and one pertaining to Counter 3. The first
part of $\Omc'_n$ can be found in Figure <ref>. We want to
achieve that for all forest models of $\Omc_n$ of finite
outdegree and all $d \in A^\Amf$, there is a pointed model $\Bmf,e$ of
$\Omc_n \cup \Omc'_n$ such that $\Bmf,e \sim^f_{\ALCO,\Sigma} \Amf,d$
if and only if one of the following holds:

* does not contain a counting tree rooted at $d$;

* Counter 2 is not properly incremented on some path in that starts at $d$;

* Counter 3 is not properly incremented on some path in that
starts at $d$.

We speak of these three options as defects of type 1, 2, and 3,
respectively. In Line (34), we choose a defect type that is present in
the current model . More precisely, being able to make $P_i$ true
at $e$ in corresponds to a defect of type $i$ in .

Lines (35)-(36) implement defects of type 1.  To see how this works,
first assume that there is a counting tree in rooted at
$d \in A^\Amf$ and let $\Bmf,e$ be a pointed model of $\Omc'_n$ with
$\Bmf,e \sim^f_{\ALCO,\Sigma} \Amf,d$. We have to argue that
$e \notin P_1^\Bmf$. This is due to Lines (35) and (36) which then
require the existence of a path in the counting tree to an element $f$
that has no $r$-successor that satisfies $S_L$ or no $r$-successor
that satisfies $S_R$, such that the maximum value of Counter 3 is not
reached on the way to $f$. But no such path exists.

For the converse, assume that for some $d \in A^\Amf$, there is a no
counting tree in rooted at $d$. This implies the existence of a
word $w \in \{L,R\}^*$ of length strictly less than $m$ such that
there is no path $p$ in starting at $d$ that follows branching
pattern $L,R$ and ends in an element where Counter 3 has maximum value
and that has no $r$-successor that satisfies $S_L$ or no $r$-successor
that satisfies $S_R$. Let $\Amf|^\downarrow_d$ denote the restriction
of to the domain elements that are reachable from $d$, traveling
role names only in the forward direction. Further let be obtained
from $\Amf|^\downarrow_d$ by making $P_1$ true on every  element
on path $p$. Then is a model of $\Omc'_n$ with $d \in P_1^\Bmf$
and $\Bmf,d \sim^f_{\ALCO,\Sigma} \Amf,d$.

Lines (37)-(46) verify that, if $P_2$ is chosen in Line (34), then
there is indeed a defect of type 2. Here we use an auxiliary single
exponential counter $D_1$ based on concept names $D_0,\dots,D_{n-1}$.
Lines (37) and (38) mark the place where incrementation of Counter 2
fails using the concept name $M_0$.

Note that Line (38) ensures that $M_0$ is chosen before the last
Counter 2 sequence in the last Counter 3 sequence is reached.  When a
domain element $d$ is marked with $M_0$, this means that it is a bit
of Counter 2 such that, on some path outgoing from $d$, the
corresponding bit in the subsequent Counter 2 sequence violates
incrementation. There are two ways in which this may happen: first,
there may be no 0-bit lower than the bit marked with $M_0$, but the
corresponding bit in the subsequent Counter 2 sequence is not
toggled. Second, there may be a 0-bit lower than the bit marked with
$M_0$, but the corresponding bit in the subsequent Counter 2 sequence
is toggled. These two cases are distinguished by Lines (40) and (41).
In the first case, the value of $X_2$ is stored in $NX_2$. In the
second case, the toggled value of $X_2$ is stored in $NX_2$. The
counter $D_1$ is then reset in Line (39) and incremented in Line (42)
to identify the corresponding bit in the following
configuration. Through lines (43) and (44), the value of $NX_2$ is
passed on all the way to this bit.  Finally, Lines (45) and (46)
ensure that the $X_2$-value of the corresponding bit coincides with
$NX_2$.  It is not so difficult to prove formally that this works. In
particular, if there is a path starting at some $d \in A^\Amf$ on
which Counter 2 is not properly incremented, then we can extend
$\Amf|^\downarrow_d$ in a straightforward way to a model of
$\Omc'_n$ with $d \in P_2^\Bmf$, by interpreting the concept names in
$\text{sig}(\Omc'_n) \setminus \text{sig}(\Omc_n)$.

\begin{eqnarray}
P_3 &\sqsubseteq& M_0 \sqcup \exists r . ((S_L \sqcup S_R) \sqcap P_3)\\
P_3 & \sqsubseteq& \neg L_3 \\[2mm]
M_0 &\sqsubseteq& (C_1=0) \sqcap M_1 \sqcap (M_L \sqcup M_R) \\
K &\sqsubseteq& \forall r . K \qquad \text{ for all } K \in
\{M_L,M_R\} \\[2mm]
%  M_R &\sqsubseteq& \forall r . M_R \\
M_1 & \sqsubseteq& (D_1=C_1) \sqcap (NX_2 \leftrightarrow X_2) \sqcap
(NX_3 \leftrightarrow X_3)\\
M_1 \sqcap (C_1 < 2^n-1) &\sqsubseteq& \exists r . ((S_L \sqcup S_R)
\sqcap M_1) \sqcap \exists r . ((S_L \sqcup S_R) \sqcap M_2)\\
% M_1 \sqcap M_2 &\sqsubseteq& \bot \\
M_2 \sqcap \neg E_3 &\sqsubseteq & \exists r . ((S_L \sqcup S_R) \sqcap M_2) \\[2mm]
M_i \sqcap K&\sqsubseteq&
\forall
. (M_i
\rightarrow
K) \quad
\text{ for all } i \in
\{2,3,4\} \text{ and} \\
&& K \in \{ C, \neg C \mid C \in
\{D_0,\dots,D_{n-1},NX_2,NX_3 \} \}\\[2mm]
M_2 \sqcap M_L \sqcap E_3 &\sqsubseteq& \exists r. (S_L \sqcap M_3) \\
M_2 \sqcap M_R \sqcap E_3 &\sqsubseteq& \exists r. (S_R \sqcap M_3)
%  \\
%  M_3 & \sqsubseteq& M_4 \sqcup \exists r . M_3 \\
%    M_3 &\sqsubseteq& \forall r . (M_2
%                                                      \rightarrow
%                                                      D_1{=}{=}) \\
%  M_3 \sqcap K&\sqsubseteq&
%                                                                 \forall
%                                                                 r
%                                                                 . (M_2
%                                                                 \rightarrow
%                                                                 K) \quad
%                                         \text{ for all } K \in \{NX_2,
% \neg NX_2, NX_3, \neg NX_3 \}
\\[2mm]
M_3 &\sqsubseteq& \neg E_3 \sqcap (M_4 \sqcup \exists r . ((S_L \cup
S_R) \sqcap M_3) \\[2mm]
M_4 &\sqsubseteq& (C_1 = D_1) \sqcap M_5 \sqcap (X_2 \leftrightarrow NX_2)
%\sqcap (NX_3 \leftrightarrow MX_3)
\, \sqcap \\
&& (Z_3 \sqcap (X_3 \leftrightarrow \neg NX_3)) \sqcup
(\neg Z_3 \sqcap (X_3 \leftrightarrow NX_3))
\\[2mm]
M_5 \sqcap (C_1 < 2^n-1) &\sqsubseteq& \exists r . ((S_L \sqcup S_R) \sqcap M_5) \\
M_5 \sqcap (C_1 = 2^n-1) &\sqsubseteq& \{ c \}
% M_4 &\sqsubseteq& (C_1=0) \\
% M_4 \sqcap \neg (C_1 = D_1) & \sqsubseteq & \exists r . ((S_L \sqcup S_R) \sqcap M_4) \\
% M_4 \sqcap (C_1 = D_1) & \sqsubseteq & M_5 \sqcap (X_2 \leftrightarrow NX_2)
%                                        %\sqcap (NX_3 \leftrightarrow MX_3)
%                                        \, \sqcap \\
%     && (Z_3 \sqcap (X_3 \leftrightarrow NX_3)) \sqcup
%        (\neg Z_3 \sqcap (X_3 \leftrightarrow \neg NX_3))
% \\[2mm]
% M_5 \sqcap (C_1 < 2^n-1) &\sqsubseteq& \exists r . ((S_L \sqcup S_R) \sqcap M_5) \\
% M_5 \sqcap (C_1 = 2^n-1) &\sqsubseteq& \{ c \}
\end{eqnarray}

The second part of ontology $\Omc'_n$.

The part of $\Omc'_n$ that is concerned with Counter 3 is displayed in
Figure <ref>. It makes sure that if $P_2$ is chosen in
Line (34), then there is indeed a defect of type 3. It is here that
using a  nominal is crucial. Lines (47) and (48) mark the place where
incrementation of Counter 3 fails using the concept name $M_0$. Note
that Line (48) ensures that $M_0$ is chosen in some Counter 3 sequence
that is not the final one; we refer to it as the `current' Counter 3
sequence.  Line (49) further makes sure that the element chosen by
$M_0$ is at the beginning of a Counter 2 sequence, which we refer to
as the `current' Counter 2 sequence. It also chooses via the concept
names $M_L$ and $M_R$ whether the defect occurs in the subsequent
Counter 3 sequence that is a left child of the current sequence, or a
right child. The chosen value is memorized `forever' in Line (50). Our
aim is to set another marker at the beginning of a Counter 2 sequence
in a subsequent Counter 3 sequence that encodes the same Counter 2
value as the current Counter 2 sequence, and then to compare the two
$X_3$-bit values of the two Counter 2 sequences.

To achieve this, we need to memorize for later comparison all
(exponentially many) $X_2$-bit values of the current Counter 2
sequence. This cannot be done in a single type and thus we use
multiple types. This is implemented in Lines (51)-(55) in which the
current Counter 2 sequence is traversed from beginning to end. In each
step, a branching takes place via Line (52). It is important to
understand that this branching is in model , but not necessarily
in model . Recall that we are interested in models that have
a functional $\ALCO,\Sigma$-bisimulation to . Informally, we can
assume the two models to have the same domain and $r$-structure up to
the element $d$ in in which we have chosen to set the marker
$M_0$.[Please compare this to defects of type 1 and 2 where
can be assumed to have the same domain and $r$-structure as ; this is also the
case here, up to the $M_0$ marker, but not beyond.]
When setting
$M_0$, then we `are' in an element $e$ of that is
$\Sigma$-bisimilar to $d$. This and what follows is illustrated in
Figure <ref>. Now Line (52) creates two $r$-successors
$f_1$ and $f_2$ of $e$ in that are both $\Sigma$-bisimilar to
$r$-successors of $d$ in . We shall argue a bit later that this
must actually be the same $r$-successor of $d$. In branch $f_1$ of
, we stay with marker $M_1$ while in branch $f_2$ of , we
switch to marker $M_2$. The $M_1$-branch branches again at the next
point of the Counter 2 sequence while the $M_2$ path does not, and so
on. Via Line (51), at each point of the Counter 2 sequence we memorize
in the newly generated $M_1$-branch the value of Counter 1 in the
auxiliary counter $D_1$, the value of $X_2$ in $NX_2$, and the value
of $X_3$ in $NX_3$. In contrast, the $M_2$-branches retain their
memory via Lines (54)-(55).  At the end of the Counter 2 sequence
whose beginning is marked with $M_0$, we have thus generated $2^n$
branches in , each storing the $X_2$-bit value for one bit
position of Counter 2, and all of them storing the $X_3$-bit value of
the current Counter 2 sequence.

Via Line (53), all the $M_2$-branches extend also beyond the current
Counter 2 sequence to the end of the current Counter 3 sequence.  In
Lines (56) and (57), we make a step to the first element of a
subsequent Counter 3 sequence, switching to marker $M_3$. All
$M_2$-branches in decide to go to an $S_L$-labeled such
subsequent sequence or all decide to go to an $S_R$-labeled such
sequence, depending on whether we had initially (before the branching)
chosen marker $M_L$ or $M_R$. Via Line (58), we proceed down the
Counter 3 sequence and set the $M_4$-marker before reaching its end.
What we want to achieve is that the $M_4$-marker is set at the
Counter 2 subsequence that carries the same Counter 2 value as the
Counter 2 sequence, at the Counter 2 bit position that the current
branch has stored in counter $D_1$. We verify independently for each
branch in that the bit position is correct, in Lines (59)-(60),
and there we also make sure that the $X_2$-bit value coincides with
the $X_2$-bit value stored in $NX_2$. We also use Line (60) to make
sure that there is indeed an incrementation conflict of Counter 3 at
this position.

We are done if we can additionally guarantee that the different
branches in have really set the $M_4$-marker at the same
Counter 2 subsequence in the same path of . So far, however, we do
not not know that this is the case, nor that the different branches
have even followed the same path of . But this is now easily
rectified: Lines (61) and (62) force all branches of to further
follow the current Counter 2 sequence, until it's end, and that the
individual name $c$ is satisfied at the end of all branches. Thus the
end of all branches is the same element in , which is functionally
bisimilar to some element of . But is a forest model and, as
$\Omc_1$ does not use nominals, it is (by definition) even a tree
model.  Consequently, on every branch of , the $r$-predecessor of
the final element marked with $c$ is functionally bisimilar to the
same element of , and so on, all the way up to the element of where the $M_0$-marker was set.

every picture/.style=line width=0.5pt

(489.03,61.43) – (475.31,78.43) ;
[shift=(473.43,80.76), rotate = 308.9] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(504.43,61.86) – (518.14,78.86) ;
[shift=(520.03,81.19), rotate = 231.1] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(470.46,84.57) – (456.74,101.57) ;
[shift=(454.86,103.9), rotate = 308.9] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(521.57,83.57) – (535.29,100.57) ;
[shift=(537.17,102.9), rotate = 231.1] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(510.74,83.43) – (497.03,100.43) ;
[shift=(495.14,102.76), rotate = 308.9] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(492.74,109.14) – (492.96,123.33) ;
[shift=(493,126.33), rotate = 269.14] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(538.46,107.14) – (524.74,124.14) ;
[shift=(522.86,126.48), rotate = 308.9] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(543.86,107.29) – (557.57,124.28) ;
[shift=(559.46,126.62), rotate = 231.1] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(454.74,109.14) – (454.96,123.33) ;
[shift=(455,126.33), rotate = 269.14] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

[dash pattern=on 4.5pt off 4.5pt]  (455,130.19) – (455.22,199.5) ;

[dash pattern=on 4.5pt off 4.5pt]  (493,130.19) – (493.22,199.5) ;

[dash pattern=on 4.5pt off 4.5pt]  (523,130.19) – (523.22,199.5) ;

[dash pattern=on 4.5pt off 4.5pt]  (560,130.19) – (560.22,199.5) ;

[dash pattern=on 4.5pt off 4.5pt]  (455.22,201.83) – (455.22,249.17) ;

[dash pattern=on 4.5pt off 4.5pt]  (493.22,201.83) – (493.22,249.17) ;

[dash pattern=on 4.5pt off 4.5pt]  (523.22,201.83) – (523.22,249.17) ;

[dash pattern=on 4.5pt off 4.5pt]  (560.22,201.83) – (560.22,249.17) ;

(455.22,249.17) – (455.43,263.36) ;
[shift=(455.48,266.36), rotate = 269.14] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(493.22,249.17) – (493.43,263.36) ;
[shift=(493.48,266.36), rotate = 269.14] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(523.22,249.17) – (523.43,263.36) ;
[shift=(523.48,266.36), rotate = 269.14] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(560.22,249.17) – (560.43,263.36) ;
[shift=(560.48,266.36), rotate = 269.14] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(455.22,269.17) – (455.43,283.36) ;
[shift=(455.48,286.36), rotate = 269.14] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(493.22,269.17) – (493.43,283.36) ;
[shift=(493.48,286.36), rotate = 269.14] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(523.22,269.17) – (523.43,283.36) ;
[shift=(523.48,286.36), rotate = 269.14] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(560.22,269.17) – (560.43,283.36) ;
[shift=(560.48,286.36), rotate = 269.14] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(492.89,289.5) – (503.29,301.87) ;
[shift=(505.22,304.17), rotate = 229.94] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(524.89,289.5) – (514.49,301.87) ;
[shift=(512.56,304.17), rotate = 310.06] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(456.22,290.17) – (492.74,303.47) ;
[shift=(495.56,304.5), rotate = 200.02] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(561.56,290.17) – (525.04,303.47) ;
[shift=(522.22,304.5), rotate = 339.98] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

[fill=rgb, 255:red, 0; green, 0; blue, 0   ,fill opacity=1 ] (499.68,55.54) .. controls (499.68,53.86) and (498.32,52.5) .. (496.64,52.5) .. controls (494.96,52.5) and (493.6,53.86) .. (493.6,55.54) .. controls (493.6,57.22) and (494.96,58.58) .. (496.64,58.58) .. controls (498.32,58.58) and (499.68,57.22) .. (499.68,55.54) – cycle ;

[dash pattern=on 4.5pt off 4.5pt]  (496.5,15.58) – (496.5,50) ;

(273.67,7.83) – (275.87,172.73) ;

(273.67,7.83) – (282.44,7.94) ;

(275.87,172.73) – (284.64,172.84) ;

(276,199.5) – (275.2,359.93) ;

(275.67,199.5) – (284.44,199.61) ;

[dash pattern=on 0.84pt off 2.51pt]  (496.64,55.54) – (309.23,54.92) ;
[shift=(307.23,54.92), rotate = 360.19] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (10.93,-4.9) .. controls (6.95,-2.3) and (3.31,-0.67) .. (0,0) .. controls (3.31,0.67) and (6.95,2.3) .. (10.93,4.9)   ;

[dash pattern=on 0.84pt off 2.51pt]  (520.03,81.19) – (308.77,80.21) ;
[shift=(306.77,80.2), rotate = 360.27] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (10.93,-4.9) .. controls (6.95,-2.3) and (3.31,-0.67) .. (0,0) .. controls (3.31,0.67) and (6.95,2.3) .. (10.93,4.9)   ;

[dash pattern=on 0.84pt off 2.51pt]  (537.17,102.9) – (309.3,103) ;
[shift=(307.3,103), rotate = 359.98] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (10.93,-4.9) .. controls (6.95,-2.3) and (3.31,-0.67) .. (0,0) .. controls (3.31,0.67) and (6.95,2.3) .. (10.93,4.9)   ;

[dash pattern=on 0.84pt off 2.51pt]  (560.15,126.62) – (309.03,125.81) ;
[shift=(307.03,125.8), rotate = 360.19] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (10.93,-4.9) .. controls (6.95,-2.3) and (3.31,-0.67) .. (0,0) .. controls (3.31,0.67) and (6.95,2.3) .. (10.93,4.9)   ;

[dash pattern=on 0.84pt off 2.51pt]  (560.66,199.5) – (308.77,199.8) ;
[shift=(306.77,199.8), rotate = 359.93] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (10.93,-4.9) .. controls (6.95,-2.3) and (3.31,-0.67) .. (0,0) .. controls (3.31,0.67) and (6.95,2.3) .. (10.93,4.9)   ;

[dash pattern=on 0.84pt off 2.51pt]  (560.66,269.17) – (308.77,267.81) ;
[shift=(306.77,267.8), rotate = 360.31] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (10.93,-4.9) .. controls (6.95,-2.3) and (3.31,-0.67) .. (0,0) .. controls (3.31,0.67) and (6.95,2.3) .. (10.93,4.9)   ;

[dash pattern=on 0.84pt off 2.51pt]  (561.56,290.17) – (308.5,288.22) ;
[shift=(306.5,288.2), rotate = 360.44] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (10.93,-4.9) .. controls (6.95,-2.3) and (3.31,-0.67) .. (0,0) .. controls (3.31,0.67) and (6.95,2.3) .. (10.93,4.9)   ;

[dash pattern=on 0.84pt off 2.51pt]  (497.11,314.67) – (309.03,314.6) ;
[shift=(307.03,314.6), rotate = 360.02] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (10.93,-4.9) .. controls (6.95,-2.3) and (3.31,-0.67) .. (0,0) .. controls (3.31,0.67) and (6.95,2.3) .. (10.93,4.9)   ;

[dash pattern=on 4.5pt off 4.5pt]  (291.33,29.67) – (291.67,49.25) ;
[shift=(291.67,49.25), rotate = 269.02] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (0,5.59) – (0,-5.59)   ;

(291.83,54.92) – (291.83,77.42) ;
[shift=(291.83,80.42), rotate = 270] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;
[shift=(291.83,54.92), rotate = 270] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (0,5.59) – (0,-5.59)   ;

(291.83,80.42) – (291.83,100.92) ;
[shift=(291.83,103.92), rotate = 270] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(291.83,103.92) – (291.83,124.42) ;
[shift=(291.83,127.42), rotate = 270] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(286.4,127.63) – (297.4,127.63) ;

[dash pattern=on 4.5pt off 4.5pt]  (291.87,169.13) – (291.9,133.45) ;
[shift=(291.9,133.45), rotate = 450.05] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (0,5.59) – (0,-5.59)   ;

[dash pattern=on 4.5pt off 4.5pt]  (295.33,225.67) – (295.13,245.93) ;
[shift=(295.13,245.93), rotate = 270.57] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (0,5.59) – (0,-5.59)   ;

(294.83,249.92) – (294.83,269.79) ;
[shift=(294.83,272.79), rotate = 270] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;
[shift=(294.83,249.92), rotate = 270] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (0,5.59) – (0,-5.59)   ;

(294.83,272.79) – (294.83,290.86) ;
[shift=(294.83,293.86), rotate = 270] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(294.83,293.86) – (294.83,311.94) ;
[shift=(294.83,314.94), rotate = 270] [fill=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.08]  [draw opacity=0] (5,-2.5) – (0,0) – (5,2.5) – (3.5,0) – cycle    ;

(289.4,315.13) – (300.4,315.13) ;

[dash pattern=on 4.5pt off 4.5pt]  (294.87,355.13) – (294.9,319.45) ;
[shift=(294.9,319.45), rotate = 450.05] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (0,5.59) – (0,-5.59)   ;

[dash pattern=on 0.84pt off 2.51pt]  (560.22,246.17) – (308.32,246.46) ;
[shift=(306.32,246.47), rotate = 359.93] [color=rgb, 255:red, 0; green, 0; blue, 0   ][line width=0.75]    (10.93,-4.9) .. controls (6.95,-2.3) and (3.31,-0.67) .. (0,0) .. controls (3.31,0.67) and (6.95,2.3) .. (10.93,4.9)   ;

(275.67,359.5) – (284.44,359.61) ;

(500.93,37.33) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{0} ,M_{1}$;

(445.6,63) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{2}$;

(522.6,67) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{1}$;

(543.17,91.71) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{1}$;

(565.22,113.29) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{1}$;

(425.89,85.43) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{2}$;

(423.93,109.05) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{2}$;

(468.31,85.38) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{2}$;

(459.98,109.05) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{2}$;

(496.31,109.38) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{2}$;

(423.6,181.05) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{3}$;

(460.93,181.05) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{3}$;

(493.93,181.05) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{3}$;

(528.93,181.38) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{3}$;

(426.6,231.05) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{4}$;

(496.27,307.71) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{4}$;

(462.1,252.05) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{4}$;

(495.1,272.55) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle M_{4}$;

(575,21) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle \mathfrak{B}$;

(231.67,21) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] $\displaystyle \mathfrak{A}$;

(281,12.5) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] Counter 3;

(377.67,34.33) node [anchor=north west][inner sep=0.75pt]   [align=left] Bisim.;

(319.4,61.3) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] Counter 2;

(284,208.5) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] Counter 3;

(319.23,250.8) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] Counter 2;

Strategy for comparing bit values of Counter 3

Based on what was said above, it can be verified that
Lemma <ref> indeed holds. We refrain from giving

§.§ -Hardness

An Alternating Turing Machine (ATM) is of the form $\mathcal{M}
= (Q,\Sigma,\Gamma,q_0,\Delta)$. The set of states $Q =
Q_\exists \uplus Q_\forall \uplus \{q_a\} \uplus \{q_r\}$ consists of
existential states from $Q_\exists$, universal states
from $Q_\forall$, an accepting state $q_a$, and a
rejecting state $q_r$; $\Sigma$ is the input alphabet
and $\Gamma$ the work alphabet containing a blank symbol
$\square$ and satisfying $\Sigma \subseteq \Gamma$; $q_0 \in
Q_\exists$ is the starting state; and the transition
relation $\delta$ is of the form

\delta \; \subseteq \; Q \times \Gamma \times Q \times \Gamma
\times \{ L,R \}.

We write $\delta(q,a)$ for
$\{ (q',b,M) \mid (q,a,q',b,M) \in \delta \}$.  As usual, we assume
that $q \in Q_\exists \cup Q_\forall$ implies
$\delta(q,b) \neq \emptyset$ for all $b \in \Gamma$ and
$q \in \{ q_a,q_r \}$ implies $\delta(q,b) = \emptyset$ for all
$b \in \Gamma$. For what follows, we also assume w.l.o.g. that for
each $q \in Q_\forall \cup Q_\exists$ and each $b \in \Sigma$, the set
$\delta(q,b)$ has exactly two elements. We assume for notational convenience that
these elements are ordered, i.e., $\delta(q,b)$ is an ordered pair

A configuration of an ATM is a word $wqw'$ with $w,w' \in
\Gamma^*$ and $q \in Q$. The intended meaning is that the tape
contains the word $ww'$ (with only blanks before and behind it), the
machine is in state $q$, and the head is on the leftmost symbol of
$w'$. The successor configurations of a configuration $wqw'$
are defined in the usual way in terms of the transition relation
$\delta$. A halting configuration is of the form $wqw'$
with $q \in \{ q_a, q_r \}$.

A computation path of an ATM $\mathcal{M}$ on a word $w$ is a
(finite or infinite) sequence of configurations $c_1,c_2,\dots$ such
that $c_1=q_0w$ and $c_{i+1}$ is a successor configuration of $c_i$
for $i \geq 0$.  All ATMs considered in this paper have only
finite computation paths on any input. A halting configuration
is accepting iff it is of the form $wq_aw'$.  For non-halting
configurations $c=w q w'$, the acceptance behaviour depends on $q$: if
$q \in Q_\exists$, then $c$ is accepting iff at least one successor
configuration is accepting; if $q \in Q_\forall$, then $c$ is
accepting iff all successor configurations are accepting.  Finally,
the ATM $\mathcal{M}$ with starting state $q_0$ accepts the
input $w$ iff the initial configuration $q_0w$ is accepting.
We use $L(\Mmc)$ to denote the language accepted by , i.e.,
$L(\Mmc) = \{ w \in \Sigma^* \mid \Mmc \text{ accepts } w \}$.

To obtain a witness for the acceptance of an input by an ATM, it is
common to arrange configurations in a tree.  Such an acceptance
tree of an ATM $\mathcal{M}$ with starting state $q_0$ on a word
$w$ is a finite tree whose nodes are labelled with configurations such

* the root node is labelled with the initial configuration $q_0w$;

* if a node $s$ in the tree is labelled with $wqw'$,
$q \in Q_\forall$, then $s$ has exactly two successors, labeled with
the two successor configurations of $wqw'$;

* if a node $s$ in the tree is labelled with $wqw'$, $q \in
Q_\exists$, then $s$ has exactly two successors, both
labelled with a successor configuration of $wqw'$;[A single
successor would of course be sufficient; we only use two
successors (which can carry the same label) to enable a more
uniform reduction.]

* leaves are labelled with accepting halting configurations.

It is clear that there exists an acceptance tree of $\mathcal{M}$ on
$w$ if and only if $\mathcal{M}$ accepts $w$.

According to Theorem 3.4 of [7], there is a double
exponentially space bounded ATM $\mathcal{M}$ whose word problem is
-hard.  We may w.l.o.g. assume that the length of every
computation path of $\mathcal{M}$ on any input $w \in \Sigma^n$ is
bounded by $2^{2^{2^n}}$, and all the configurations $wqw'$ in such
computation paths satisfy $|ww'| \leq 2^{2^n}$.

We prove Theorem <ref> by reduction from the word
problem for . Thus let $w \in \Sigma^*$ be an input to
$\mathcal{M}$.  We have to construct an -ontology $\Omc$ and an
-ontology $\Omc'$ such that $\Omc \cup \Omc'$ is a conservative
extension of $\Omc$ if and only if $M$ does not accept $w$.  This can
be achieved by extending the ontologies $\Omc_n$ and $\Omc'_n$ from
Section <ref>, where $n$ is the length of $w$.  The
main idea is to do this such that models of witness concepts for
$\Omc$ and $\Omc'$ describe an acceptance tree of $\mathcal{M}$ on $w$
instead of a counting tree. In fact, such models describe a tree
that is a counting tree and at the same time a computation tree. We
again use only a single role name $r$. Each configuration of is
represented by a Counter 3 sequence and each tape cell of a
configuration is represented by a Counter 2 sequence. Thus, each node
of the acceptance tree is spread out over $2^n \cdot 2^{2^n}$ elements
in the model and the role name $r$ might indicate moving to the next
tape cell in the same configuration, moving to the first tape cell of
a successor configuration, and also moving to the next element in the
Counter 2 sequence that represents the current tape cell.

So we only need to represent the computation of on $w$ on top of
a counting tree that we have already enforced by $\Omc_n$ and
$\Omc'_n$, and we can exploit the three counters that $\Omc_n$ and
$\Omc'_n$ give us. Such a representation is in fact fairly standard
and no additional technical tricks are needed, see for instance the
-hardness proof for conservative extensions in given
in [12]. Since fully worked out concept inclusions are
nevertheless lengthy and difficult to comprehend, we only sketch the
required extensions of $\Omc_n$ and $\Omc'_n$.

In the extension of $\Omc_n$, we use an additional concept name
$S_q$ for every state $q \in Q$, $S_a$ for every symbol $a \in
\Sigma$, and $H$ for indicating the head position. The ontology then makes sure that all these symbols are interpreted uniformly in
Counter 2 sequences, that exactly one concept name $S_a$ is true at
every Counter 2 sequence, and that there is exactly one Counter 2
sequence in each Counter 3 sequence where $H$ is true, together with a
unique concept name $S_q$. It also guarantees that the computation
starts with the initial configuration $q_0w$. All remaining properties
of computation trees are achieved by $\Omc'$. In preparation for this,
we add more concept names to , namely primed versions $S'_q$,
$S'_q$, and $H'$ of all concept names introduced above as well as
concept names $Y_{q,a,M}$ and $Y_{q,a,M}$ for all $q \in Q$, $a \in
\Sigma$, and $M \in \{L,R\}$. Informally, a concept name $Y_{q,a,M}$
indicates that for moving to the current configuration, the Turing
machine has decided to write symbol $a$, switch to state $q$, and move
in direction $M$.  Still in $\Omc$, we make sure that the primed
concept names satisfy the same constraints as their unprimed siblings,
that the concept names $Y_{q,a,M}$ are set in successor configurations
(Counter 3 sequences) in accordance with the unprimed concept names
and the transition relation, and that if some $Y_{q,a,M}$ is set in
the current configuration, then the non-primed and the primed concept
names relate to each other accordingly.

It remains for $\Omc'$ to make sure that the transition relation of
is respected and that the the rejecting state is not reached on
any branch. Given what was already done in , the former can be
achieved by enforcing that whenever some unprimed concept name
$S_q$, $S_a$, or $H$ is true in some Counter 2 sequence, then its
primed version is true in the Counter 2 sequence that represents
the same Counter 2 value of all subsequent Counter 3 sequences.
We refer to this as correct copying.

Strictly speaking, the second ontology $\Omc'$ is not an extension of
because we need to replace Line (34) with the following, which
admits five different types of defects in place of two:

A \sqsubseteq P_1 \sqcup P_2 \sqcup P_3 \sqcup P_4 \sqcup P_5.

$P_4$ is for checking that some branch reaches the rejecting state.
This is easy to implement, using existential restrictions as in
Lines (37)-(46) (rather than universal restrictions as in Lines (35)
and (36)). $P_5$ is for verifying that correct copying is taking
place. This is achieved by a slight variation of the concept
inclusions in Figure <ref> (which also use existential
restrictions). In fact, those concept inclusions can be viewed as
copying the value of an $X_3$-bit to same-value Counter 2
subsequences of subsequent Counter 3 sequences. We copy
the information stored in the concept names $S_q$, $S_a$, and $H$

§ PROOFS FOR SECTION <REF>

The upper bound follows from the fact that the
complement of the problem to decide $\varphi_{\Kmc,\Sigma,a}(x) \models \neg \varphi_{\Kmc,\Sigma,b}(x)$ can be equivalently formulated as a concept
satisfiability problem in the extension $\mathcal{ALCIO}^{u}$ of $\mathcal{ALCIO}$ with the universal
role $u$. To see this, obtain $C_{\Kmc,\Sigma,a}$
from $\Kmc$ by taking the conjunction of the following concepts:

* $\forall u.(C \rightarrow D)$, for $C \sqsubseteq D\in \Omc$;

* $\forall u.(\{c\}\rightarrow \exists R.\{d\})$, for $R(c,d)\in \Dmc$;

* $\forall u.(\{c\}\rightarrow A)$, for $A(c)\in \Dmc$;

and then replacing

* all concept and role names $X$ not in $\Sigma$ by
fresh and distinct symbols $X_{a}$;

* all individual names $c$ not in $\Sigma\cup \{a\}$ by fresh and distinct individual names $c_{a}$;

* the individual name $a$ by a fresh individual name $m$;

* if $a\in \Sigma$ then add $\{m\} \leftrightarrow \{a\}$ as a conjunct.

Define $C_{\Kmc,\Sigma,b}$ in the same way with $a$ replaced by $b$.
Then $\varphi_{\Kmc,\Sigma,a}(x) \wedge \varphi_{\Kmc,\Sigma,b}(x)$ is satisfiable if $m \wedge C_{\Kmc,\Sigma,a}\wedge C_{\Kmc,\Sigma,b}$ is satisfiable.

“2. $\Rightarrow$ 1.” is trivial. For the converse direction, assume that Condition 1. holds.

Note that we can view $\Kmc_{\Sigma,a}$ as the union of $\Omc_{a}$ and $\Dmc_{a}$, where

* $\Omc_{a}$ is a copy of $\Omc$ in which all concept and role names  $X\not\in \Sigma$ have been replaced by fresh symbols $X_{a}$;

* $\Dmc_{a}$ is a copy of $\Dmc$ in which every concept and role name $X\not\in \Sigma$ is replaced by $X_{a}$ and in which every individual $c\not\in \Sigma\cup \{a\}$ is replaced by a variable $x_{c,a}$ and $a$ is replaced by $x$. Moreover, $x=a$ is added if $a\in \Sigma$.

Thus, by taking the conjunction of all members of $\Dmc_{a}$ and existentially quantifying over all variables distinct from $x$ we obtain a formula in CQ$^{\ALCI}$.
$\Kmc_{\Sigma,b}$ can be viewed accordingly with $a$ replaced by $b$.

In what follows we write

* $\Amf,d \Leftrightarrow_{\text{CQ}^{\ALCIO},\Sigma} \Bmf,e$ if
$\Amf\models \varphi(d)$ iff $\Bmf\models \varphi(e)$, for all
$\varphi(x)$ in $\text{CQ}^{\ALCIO}(\Sigma)$.

* $\Amf,d \Leftrightarrow_{\text{CQ}^{\ALCIO},\Sigma}^{\text{mod}} \Bmf,e$
if for all finite $D\subseteq \text{dom}(\Amf)$
containing $d$ we have
$\Amf,d\rightarrow_{D,\ALCIO,\Sigma} \Bmf,e$, and vice versa.

By Condition 1, we have $\varphi_{\Kmc,\Sigma,a}(x) \models \neg\varphi_{\Kmc,\Sigma,b}(x)$. Assume there does not exist a separating formula in BoCQ$^{\mathcal{ALCIO}}(\Sigma)$. We first show the following claim.

Claim 1. There exist pointed structures $\Amf,d$ and $\Bmf,e$ such that
$\Amf\models \varphi_{\Kmc,\Sigma,a}(d)$ and
$\Bmf \models \varphi_{\Kmc,\Sigma,b}(e)$ and $\Amf,d \Leftrightarrow_{\text{CQ}^{\ALCIO},\Sigma} \Bmf,e$.

For the proof of Claim 1, consider the set $\Gamma$ of all formulas $\psi(x)$ in BoCQ$^{\mathcal{ALCIO}}(\Sigma)$ such that $\varphi_{\Kmc,\Sigma,a}(x) \models \psi(x)$. By compactness and our assumption,

\Gamma \cup \{\varphi_{\Kmc,\Sigma,b}(x)\}

is satisfiable. Take a pointed model $\Bmf,e$ of
$\Gamma \cup \{\varphi_{\Kmc,\Sigma,b}(x)\}$. Next, let $\Psi$ be the set of all
$\psi(x)$ in BoCQ$^{\mathcal{ALCIO}}(\Sigma)$ such that $\Bmf \models \psi(e)$.
By compactness and assumption

\Psi \cup\{\varphi_{\Kmc,\Sigma,a}(x)\}

is satisfiable. Take a pointed model $\Amf,d$ of $\Psi \cup\{\varphi_{\Kmc,\Sigma,a}(x)\}$.
By definition, the pointed models $\Amf,d$ and $\Bmf,e$ are as required in Claim 1.

Using $\omega$-saturated elementary extensions of the pointed models $\Amf,d$ and $\Bmf,e$ from Claim 1 we obtain the following claim using Lemma <ref>.

Claim 2. There exist pointed structures $\Amf,d$ and $\Bmf,e$ such that
$\Amf\models \varphi_{\Kmc,\Sigma,a}(d)$ and
$\Bmf \models\varphi_{\Kmc,\Sigma,b}(e)$ and such that
$\Amf,d \Leftrightarrow_{\text{CQ}^{\ALCI},\Sigma}^{\text{mod}} \Bmf,e$.

Now take assignments $v_{a}$ from the variables of $\varphi_{\Kmc,\Sigma,a}$ into
$\Amf$ witnessing $\Amf\models \varphi_{\Kmc,\Sigma,a}(d)$ and $v_{b}$ from
the variables of $\varphi_{\Kmc,\Sigma,b}$ into
$\Bmf$ witnessing $\Bmf\models \varphi_{\Kmc,\Sigma,b}(e)$. Let $D_{a}$ and $D_{b}$ be the images of $v_{a}$ in $\Amf$ and of $v_{b}$ in $\Bmf$, respectively. By definition, we have $\Sigma$-homomorphisms

* $h_{a}: \Amf_{|D_{a}} \rightarrow \Bmf$ mapping $d$ to $e$ and such  that $\Amf,c \sim_{\mathcal{ALCIO},\Sigma} \Bmf,h_{a}(c)$ for all $c\in D$;

* $h_{b}: \Bmf_{|D_{b}} \rightarrow \Amf$ mapping $e$ to $d$ and
such that $\Bmf,c \sim_{\mathcal{ALCIO},\Sigma}\Amf, h_{b}(c)$ for all $c\in D_{b}$.

We also have by definition that for any
$c\in \text{dom}(\Amf)$ there exists a $c'\in \text{dom}(\Bmf)$ such that $\Amf,c \sim_{\mathcal{ALCIO},\Sigma} \Bmf,c'$, and vice versa.
We now merge $\Amf$ and $\Bmf$ to a single structure by taking their bisimulation product $\Cmf$, defined as follows.
The domain of $\Cmf$ is

\{ (c,c') \in \text{dom}(\Amf) \times \text{dom}(\Bmf) \mid \Amf,c \sim_{\ALCI,\Sigma} \Bmf,c'\}

and we set

* $(c,c')\in A^{\Cmf}$ if $c\in A^{\Amf}$ (equivalently, if $c'\in A^{\Bmf}$) for all $A\in \Sigma$;

* $(c,c')\in A^{\Cmf}$ if $c\in A^{\Amf}$ for all $A \in \text{sig}(\varphi_{\Kmc,\Sigma,a})\setminus \Sigma$;

* $(c,c')\in A^{\Cmf}$ if  $c'\in A^{\Bmf}$ for all $A \in \text{sig}(\varphi_{\Kmc,\Sigma,b})\setminus \Sigma$;

* $((c_{1},c_{1}'), (c_{2},c_{2}')) \in r^{\Cmf}$ if $(c_{1},c_{2})\in r^{\Amf}$ and $(c_{1}',c_{2}')\in r^{\Bmf}$ for all $r\in \Sigma$;

* $((c_{1},c_{1}'), (c_{2},c_{2}')) \in r^{\Cmf}$ if $(c_{1},c_{2})\in r^{\Amf}$ for all $r\in \text{sig}(\varphi_{\Kmc,\Sigma,a})\setminus \Sigma$;

* $((c_{1},c_{1}'), (c_{2},c_{2}')) \in r^{\Cmf}$ if $(c_{1}',c_{2}')\in r^{\Bmf}$ for all $r\in \text{sig}(\varphi_{\Kmc,\Sigma,b})\setminus\Sigma$;

* $c^\Cmf = (c^{\Amf},c^{\Bmf})$ for all $c\in \Sigma$.

We show that $\Cmf\models (\varphi_{\Kmc,\Sigma,a}\wedge \varphi_{\Kmc,\Sigma,b})(d,e)$ which contradicts the assumption that
$\varphi_{\Kmc,\Sigma,a}(x)\models \neg \varphi_{\Kmc,\Sigma,b}(x)$.
To show that $\Cmf$ is a model of $\Omc_{a}$ and $\Omc_{b}$ it suffices to show
the following claim.

Claim 3. (1) The projection $p_{a}:\Cmf \rightarrow \Amf$ defined by setting $p_{a}(c,c')=c$ is an $\mathcal{ALCIO}(\text{sig}(\varphi_{\Kmc,\Sigma,a}))$-bisimulation between $\Cmf$ and $\Amf$.

(2) The projection $p_{b}:\Cmf \rightarrow \Bmf$ defined by setting $p_{b}(c,c')=c'$ is an $\mathcal{ALCIO}(\text{sig}(\varphi_{\Kmc,\Sigma,b}))$-bisimulation between $\Cmf$ and $\Bmf$.

The proof of Claim 3 is straightforward and omitted. It follows from Claim 3 and the assumption that $\Amf$ is a model of $\Omc_{a}$ and $\Bmf$ a model of $\Omc_{b}$ that $\Cmf$ is a model of $\Omc_{a}\cup \Omc_{b}$.

Next we lift the variable assignments $v_{a}$ and $v_{b}$ from $\Amf$ and, respectively, $\Bmf$ to $\Cmf$. Thus, we set

* $\bar v_{a}(x_{c})= (v_{a}(x_{c}),h_{a}(v_{a}(x_{c}))$ for all variables of the form $x_{c}$ in $\varphi_{\Kmc,\Sigma,a}$ and

* $\bar v_{b}(y_{c})= (v_{b}(y_{c}),h_{b}(v_{b}(y_{c}))$ for all variables of the form $y_{c}$ in $\varphi_{\Kmc,\Sigma,b}$.

* $\bar v_{a}(x)=\bar v_{b}(x) = (v_{a}(x),v_{b}(x))$.

The following claim is straightforward now.

Claim 4. $\Cmf\models_{\bar v_{a}} \Dmc_{a}(d,e)$ and $\Cmf\models_{\bar v_{b}} \Dmc_{b}(d,e)$.

Claim 4 implies $\Cmf\models (\varphi_{\Kmc,\Sigma,a}\wedge \varphi_{\Kmc,\Sigma,b})(d,e)$ as we have established already that $\Cmf$ is
a model of $\Omc_{a}\cup \Omc_{b}$.
This concludes the proof.

We first prove the upper bounds. To this end, we formulate the complexity results proved in [3] for interpolant existence in detail. Let $\Lmc\in \DLS$.
Let $\Omc_{1},\Omc_{2}$ be $\Lmc$-ontologies and let $C_{1},C_{2}$ be $\Lmc$-concepts. Let $\Sigma= \text{sig}(\Omc_{1},C_{1}) \cap \text{sig}(\Omc_{2},C_{2})$. An $\Lmc$-interpolant for the $\Lmc$-tuple $\Omc_{1},\Omc_{2},C_{1},C_{2}$ is an $\Lmc(\Sigma)$-concept $C$ such that

* $\Omc_{1} \models C_{1} \sqsubseteq C$;

* $\Omc_{2} \models C \sqsubseteq C_{2}$.

The following is shown in [3].

Let $\Lmc\in \DLS$. Then the problem to decide whether an $\Lmc$-interpolant
exists for $\Lmc$-tuples $\Omc_{1},\Omc_{2},C_{1},C_{2}$ is -complete.

Now assume that $\Lmc\in \DLS$ and a labeled $\Lmc$-KB $(\Kmc,\{a\},\{b\})$ with $\Kmc=(\Omc,\Dmc)$ and $\Sigma\subseteq \text{sig}(\Kmc)$ are given. Let $\Lmc\Omc$ denote the extension of $\Lmc$ by nominals (if $\Lmc$ contains nominals already then set $\Lmc\Omc=\Lmc$).
Obtain an $\Lmc\Omc$-ontology $\Omc_{\Kmc,\Sigma,a}$ from $\Kmc$ by taking the following inclusions:

* all inclusions in $\Omc$;

* $\{c\}\sqsubseteq \exists R.\{d\}$, for $R(c,d)\in \Dmc$;

* $\{c\}\sqsubseteq A$, for $A(c)\in \Dmc$;

and then replacing

* all concept and role names $X$ not in $\Sigma$ by
a fresh symbol $X_{a}$;

* all individuals $c$ not in $\Sigma\cup \{a\}$ by fresh and distinct individuals $c_{a}$;

* the individual $a$ by a fresh individual $m_{a}$. If
$a\in \Sigma$ then the CI $\{m_{a}\} \equiv \{a\}$ is added.

$\Omc_{\Kmc,\Sigma,b}$ is obtained from $\Kmc$ in the same way by replacing $a$ by $b$.
Observe that an $\Lmc\Omc(\Sigma)$-concept strongly separates $(\Kmc,\{a\},\{b\})$ iff it is an $\Lmc\Omc$-interpolant for the $\Lmc\Omc$-tuple $\Omc_{\Kmc,\Sigma,a}$, $\Omc_{\Kmc,\Sigma,b}$, $m_{a},\neg m_{b}$. If $\Lmc$ contains nominals, then the upper bounds stated in Theorem <ref> follow immediately. If $\Lmc$ does not contain nominals, then we may assume that $\Sigma$ does not contain individual names.
Then $\Omc_{\Kmc,\Sigma,a}$ and $\Omc_{\Kmc,\Sigma,b}$ do not share any
individual names and therefore an $\Lmc(\Sigma)$-concept strongly separates $(\Kmc,\{a\},\{b\})$ iff it is an $\Lmc\Omc$-interpolant for the $\Lmc\Omc$-tuple $\Omc_{\Kmc,\Sigma,a}$, $\Omc_{\Kmc,\Sigma,b}$, $m_{a},\neg m_{b}$. Thus, the upper bound follows again.

Now we come to the lower bounds. We first give a
model-theoretic characterization of strong
$\Lmc$-separability using $\Lmc$-bisimulations.

Let $\Lmc \in \DLS$. Let $(\Kmc,\{a\},\{b\})$ be a labeled $\Lmc$-KB and $\Sigma\subseteq
\text{sig}(\Kmc)$ a signature.  Then the following conditions are

* $(\Kmc,\{a\},\{b\})$ is strongly $\Lmc(\Sigma)$-separable;

* There are no models $\Amf$ and $\Bmf$ of $\Kmc$ such that
$\Amf,a^{\Amf}\sim_{\Lmc,\Sigma} \Bmf,b^{\Bmf}$.

The proof is straightforward using Lemma <ref>.
The following result is shown as part of the lower bound proof for interpolant existence in [3]:

Let $\Lmc \in \DLS$. For $\Lmc$-ontologies $\Omc$ and database $\Dmc$ of the form $\{R(a,a)\}$ it
is -hard to decide the following: do there exist models $\Amf$ and $\Bmf$ of $(\Omc,\Dmc)$ such that
$\Amf,a^{\Amf}\sim_{\Lmc,\Sigma} \Bmf,d$ for some $d\not= a^{\Bmf}$.

-hardness of Condition 2 of Lemma <ref>
is a direct consequence of Theorem <ref>. For suppose
that $\Lmc$, $\Kmc=(\Omc,\Dmc)$, $\Sigma$, and $a$ from Theorem <ref> are given. Let $b$ be a fresh individual name and $A_{1},A_{2}$ fresh concept names. Add $A_{1}(a)$ and $A_{2}(b)$ to $\Dmc$ to obtain $\Dmc'$ and add $A_{1} \sqsubseteq \neg A_{2}$ to $\Omc$ to obtain $\Omc'$.
Then exist models $\Amf$ and $\Bmf$ of $(\Omc,\Dmc)$ such that
$\Amf,a^{\Amf}\sim_{\Lmc,\Sigma} \Bmf,d$ for some $d\not= a^{\Bmf}$
iff there exist models $\Amf$ and $\Bmf$ of $\Kmc$ such that $\Amf,a^{\Amf} \sim_{\Lmc,\Sigma} \Bmf,b^{\Bmf}$.

§ PROOFS FOR SECTION <REF>

The proof of Theorem <ref> is inspired by the proof of the
undecidability of conservative extensions and projective conservative
extensions in every extension of the three-variable
fragment GF$^3$ of GF [22]. Unfortunately, it
is not clear how to achieve a direct reduction of conservative
extensions to separability for GF. The relativization that was used
for languages in $\DLS$ does not work because non-conservativity in
GF is witnessed by sentences while separability is witnessed by open formulas.

The proof is by a reduction from the halting problem of two-register
machines. A (deterministic) two-register machine (2RM)Two-register
machine2RM is a pair $M=(Q,P)$ with $Q = q_0,\dots,q_{\ell}$
a set of states and $P = I_0,\dots,I_{\ell-1}$ a sequence of
instructions.  By definition, $q_0$ is the initial
state, and $q_\ell$ the halting state. For all $i < \ell$,

* either $I_i=+(p,q_j)$ is an incrementation instruction
with $p \in \{0,1\}$ a register and $q_j$ the subsequent state;

* or $I_i=-(p,q_j,q_k)$ is a decrementation instruction
with $p \in \{0,1\}$ a register, $q_j$ the subsequent state if
register $p$ contains 0, and $q_k$ the subsequent state otherwise.

A configuration of $M$ is a triple $(q,m,n)$, with $q$ the
current state and $m,n \in \mathbb{N}$ the register contents.  We
write $(q_i,n_1,n_2) \Rightarrow_M (q_j,m_1,m_2)$ if one of the
following holds:

* $I_i = +(p,q_j)$, $m_p = n_p +1$, and $m_{1-p} =

* $I_i = -(p,q_j,q_k)$, $n_p=m_p=0$, and $m_{1-p} =

* $I_i = -(p,q_k,q_j)$, $n_p > 0$, $m_p = n_p -1$, and
$m_{1-p} = n_{1-p}$.

The computation of $M$ on input $(n,m) \in \mathbb{N}^2$ is
the unique longest configuration sequence $(p_0,n_0,m_0)
\Rightarrow_M (p_1,n_1,m_1) \Rightarrow_M \cdots$ such that $p_0 =
q_0$, $n_0 = n$, and $m_0 = m$.

The halting problem for 2RMs is to decide, given a 2RM $M$, whether
its computation on input $(0,0)$ is finite (which implies that its
last state is $q_\ell$).

We convert a given 2RM $M$ into a labeled GF$^3$ KB
$(\Kmc,\{a\},\{b\})$, $\Kmc = (\Omc,\Dmc)$ and signature $\Sigma$ such that $M$ halts iff
$(\Kmc,\{a\},\{b\})$ is (non-)projectively GF$(\Sigma)$-separable iff
$(\Kmc,\{a\},\{b\})$ is (non-)projectively $\ALC(\Sigma)$-separable.
Let $M=(Q,P)$ with $Q = q_0,\dots,q_{\ell}$ and
$P = I_0,\dots,I_{\ell-1}$. We assume w.l.o.g. that $\ell \geq 1$ and
that if $I_i=-(p,q_j,q_k)$, then $q_j \neq q_k$. In $\Kmc$,
we use the following set of relation symbols:

* a binary symbol $N$ connecting a configuration to
its successor configuration;

* binary symbols $R_{1}$ and $R_{2}$ that represent the
register contents via the length of paths;

* unary symbols $q_{0},\ldots,q_{\ell}$ representing the states of $M$;

* a unary symbol $S$ denoting points where a computation starts.

* a unary symbol $D$ used to represent that there is
some defect;

* binary symbols $D^{+}_{p},D_{p}^{-},D_{p}^{=}$ used to
describe defects in incrementing, decrementing, and keeping
register $p\in \{0,1\}$;

* ternary symbols
$H_{1}^{+},H_{2}^{+},H_{1}^{-},H_{2}^{-},H_{1}^{=},H_{2}^{=}$ used
as guards for existential quantifiers.

The signature $\Sigma$ consists of the symbols from the first four
points above.

We define the ontology $\Omc$ as the set of several GF$^3$
sentences.[The formulas that are not syntactically guarded
can easily be rewritten into such formulas.] The first sentence
initializes the starting configuration:

\[\forall x  (Sx \rightarrow (q_0x \wedge \neg \exists y \, R_0xy
\wedge \neg \exists y \, R_1xy))\]

Second, whenever $M$ is not in the final state, there is a
next configuration with the correctly updated state. For $0 \leq i <
\ell$, we include:

$$ \begin{array}{l}
\forall x (q_ix \rightarrow \exists y\, Nxy) \\[1mm]
\forall x (q_{i}x \rightarrow \forall y (Nxy \rightarrow q_{j}y))
\hspace{1.5cm}\text{ if } I_i=+(p,q_j) \\[1mm]
\forall x ((q_{i}x \wedge \neg \exists y R_{p}xy) \rightarrow\forall
y (Nxy \rightarrow q_{j}y))\\[1mm]
\hspace{5.6cm}\text{ if } I_i=-(p,q_j,q_k) \\[1mm]
\forall x ((q_{i}x \wedge \exists y R_{p}xy)  \rightarrow \forall y
(Nxy \rightarrow q_{k}y)) \\[1mm]
\hspace{5.6cm}\text{ if } I_i=-(p,q_j,q_k) \end{array}

Moreover, if $M$ is in the final state, there is no successor

\[\forall x(q_\ell x\rightarrow \neg \exists y\,Nxy).\]

The next conjunct expresses that either $M$ does not halt or the
representation of the computation of $M$ contains a defect. It
crucially uses non-$\Sigma$ relation symbols.  It takes the shape of

\[ \forall x \, (Dx \rightarrow \exists y \, (Nxy \wedge \psi xy)) \]

where $\psi xy$ is the following disjunction which ensures that there
is a concrete defect ($D_p^+,D_p^-,D_p^=$) here or some defect ($D$)
in some successor state:

\[ \begin{array}{l}
D(y) \vee{} \\[2mm]
\displaystyle \bigvee_{I_i=+(p,q_j)} (q_ix \wedge q_jy \wedge (D^+_pxy
\vee D^=_{1-p}xy))\vee{}\\[6mm]
\displaystyle \bigvee_{I_i=-(p,q_j,q_k)} (q_ix \wedge q_ky \wedge
(D^-_pxy \vee D^=_{1-p}xy))\vee{} \\[6mm]
\displaystyle \bigvee_{I_i=-(p,q_j,q_k)} (q_ix \wedge q_jy \wedge
(D^=_pxy \vee D^=_{1-p}xy))
%  \\[6mm] \wedge \, \forall x \forall y \, (D^+_pxy \rightarrow
%  %\\[1mm] %  \hspace*{6mm} (\neg \exists z \, R_pyz \vee (\neg
%  \exists z \, R_pxz \wedge \exists z \, (R_pyz \wedge \exists x
%  R_pzx))\\[2mm] \hspace*{29mm}\vee \, \exists z (H_{1}^{+}xyz \wedge
%  R_{p}xz \wedge \exists x (H_{2}^{+}xzy \wedge R_pyx \wedge
%  D^+_{p}zx)).
\end{array} \]

Finally, using the ternary symbols we make sure that the defects are
realized, for example, by taking:

\[ \begin{array}{l}
\forall x \forall y \, \big(D^+_pxy \rightarrow \\[1mm]
\hspace*{2mm} (\neg \exists z \, R_pyz \vee (\neg \exists z \, R_pxz
\wedge \exists z \, (R_pyz \wedge \exists x R_pzx))\vee{}\\[2mm]
\hspace*{3mm} \exists z (H_{1}^{+}xyz \wedge R_{p}xz \wedge \exists x
(H_{2}^{+}xzy \wedge R_pyx \wedge D^+_{p}zx)))\big).
\end{array} \]

Similar conjuncts implement the desired behaviour of $D^=_p$ and
$D^-_p$; since they are constructed analogously to the last three
lines above (but using guards $H^{-}_j$ and $H^{=}_j$), details are

Finally, we define a database $\Dmc$ by taking

\[\Dmc = \{S(a),D(a),S(b)\}.\]

Lemmas <ref> and <ref> below establish
correctness of the reduction and thus Theorem <ref>.

If $M$ halts, then there is an $\ALC(\Sigma)$ concept that
non-projectively separates $(\Kmc,\{a\},\{b\})$.

The idea is that the separating $\ALC(\Sigma)$ concept
describes the halting computation of $M$, up to
$\ALC(\Sigma)$-bisimulations. More precisely, assume that $M$ halts.
We define an $\ALC(\Sigma)$ concept $C$ such that $\Kmc\models\neg
C(a)$, but $\Kmc\not\models\neg C(b)$.  Intuitively, $C$ represents
the computation of $M$ on input $(0,0)$, that is: if the computation
is $(q_0,n_0,m_0),\dots,(q_k,n_k,m_k)$, then there is an $N$-path of
length $k$ (but not longer) such that any object reachable in $i
\leq k$ steps from the beginning of the path is labeled with $q_i$,
has an outgoing $R_0$-path of length $n_i$ and no longer outgoing
$R_0$-path, and likewise for $R_1$ and $m_i$. In more detail,
consider the $\Sigma$-structure $\Amf$ with

\begin{align*}
\text{dom}(\Amf) = \{0,\ldots,k\} \cup {} & \{ a_{j}^{i} \mid
0<i\leq k, 0<j<n_{i}\} \cup{} \\
& \{ b_{j}^{i} \mid 0<i\leq k, 0<j< m_{i}\}
\end{align*}

in which

$$ \begin{array}{rcl}
N^{\Amf} &=& \{ (i,i+1) \mid i<k\} \\[1mm]
R_{1}^{\Amf} &=& \bigcup_{i\leq k}\{ (i,a_{1}^{i}),
\\[1mm]
R_{2}^{\Amf} &=& \bigcup_{i\leq k}\{ (i,b_{1}^{i}),
\\[1mm]
S^{\Amf} &=& \{0\} \\[1mm]
% 	E^{\Amf} &=& \{a^i_{n_i-1},b^i_{m_i-1}\mid i\leq k\}\\[1mm]
q^{\Amf} &=& \{ i \mid q_{i}=q\} \text{ for any } q\in Q.
\end{array} $$

Then let $C$ be the $\ALC(\Sigma)$ concept that describes $\Amf$
from the point of $0$ up to $\ALC(\Sigma)$-bisimulations. Clearly,
$\Kmc\cup\{C(b)\}$ is satisfiable. However, $\Kmc\cup\{C(a)\}$ is
unsatisfiable since the enforced computation does not contain a
defect and cannot be extended to have one. In particular, there are
no $N$-paths of length $>k$ in any model of $\Kmc\cup\{C(a)\}$ and
there are no defects in register updates in any model of

The following lemma implies that if $M$ does not halt, then
$(\Kmc,\{a\},\{b\})$ is neither projectively $\Lmc(\Sigma)$-separable
nor non-projectively $\Lmc(\Sigma)$-separable for $\Lmc=\text{GF}$ and
in fact for every logic between GF and FO.

If $M$ does not halt, then for every model $\Amf$ of , there is
a model $\Bmf$ of such that $(\Amf,b^\Amf)$ is
$\Gamma$-ismorphic to $(\Bmf,a^\Bmf)$ where $\Gamma$ consists of all
symbols except $\text{sig}(\Omc)\setminus \Sigma$.

Let $\Amf$ be a model of . We obtain $\Bmf$ from by
re-interpreting $a^\Bmf=b^\Amf$ and inductively defining the
extensions of the symbols from

\begin{align*}
\text{sig}(\Omc)\setminus\Sigma = \{D,D^+_p,&D^-_p,D^=_p,\\
& H_1^+,H_2^+,H_1^-,H_2^-,H_1^=,H_2^=\}.
\end{align*}

We start with $D^\Bmf = \{a^\Bmf\}$ and $X^\Bmf=\emptyset$ for all
other symbols $X$ from $\text{sig}(\Omc)\setminus \Sigma$. Then,
whenever $d\in D^\Bmf$ we distinguish two cases:

* If there is an $N$-successor $e$ of $d$ such that the
counters below $d$ and $e$ are not correctly updated with
respect to the states at $d,e$, set the extensions of the
symbols in
$D^+_p,D^-_p,D^=_p,H_1^+,H_2^+,H_1^-,H_2^-,H_1^=,H_2^=$ so as to
represent the defect and finish the construction of $\Bmf$.

* Otherwise, choose an $N$-successor $e$ of $d$ and add
$e$ to $D^\Bmf$.

Note that, since $M$ does not halt, we can always find such an
$N$-successor as in the second item.

The proof of Theorem <ref> relies on the encoding of GF and FO$^{2}$-KBs into formulas in GF and FO$^{2}$.

For Points 1 and 2 we can use the extensions of GF and FO$^{2}$ with constants as we only require Craig interpolants in FO and the upper bounds for satisfiability of GF and FO$^{2}$ still hold for their extensions with constants. We start with GF. Assume a labeled GF-KB $(\Kmc,\{a\},\{b\})$ with $\Kmc=(\Omc,\Dmc)$ is given. Let $\Sigma$ be a signature.
Obtain $\varphi_{\Kmc,\Sigma,a}'$ from
$\Kmc$ by

* replacing all relation symbols $R\not\in\Sigma$ by fresh relation symbols $R_{a}$;

* replacing all individual names $c\not\in\Sigma\cup \{a\}$ by fresh individual names $c_{a}$;

* replacing $a$ by a fresh variable $x$ and adding $x=a$ if $a\in \Sigma$;

and taking the conjunction of the resulting set of formulas.
Define $\varphi_{\Kmc,\Sigma,b}'$ in the same way but with $a$ replaced
by $b$. Then an FO-formula $\varphi$ strongly $\Sigma$-separates $(\Kmc,\{a\},\{b\})$ iff $\varphi$ is an FO-interpolant for $\varphi_{\Kmc,\sigma,a}',\neg\varphi_{\Kmc,\Sigma,b}'$, and we have proved Point 1. For Point 2, observe that $\varphi_{\Kmc,\sigma,a}',\varphi_{\Kmc,\Sigma,b}'$ are in FO$^{2}$
if $\Kmc$ is an FO$^{2}$-KB. Thus, the argument applies to FO$^{2}$ as well and we have proved Point 2.

For Points 3 and 4 we assume that $\Sigma$ is a relational signature and as we aim to apply results on the complexity of interpolant existence that have been proved for GF and FO$^{2}$ without constants we cannot use constants in the construction of the encodings.

Assume a labeled GF-KB $(\Kmc,\{a\},\{b\})$ with $\Kmc=(\Omc,\Dmc)$ is given and $\Sigma$ is a relational signature. Consider
the formulas $\varphi_{\Kmc,\Sigma,a}$ and $\varphi_{\Kmc,\Sigma,b}$ from the main paper (defined in the obvious way for GF). To obtain GF-formulas $\varphi^{\text{GF}}_{\Kmc,\Sigma,a}$ and
$\varphi^{\text{GF}}_{\Kmc,\Sigma,b}$, take
fresh relation symbols $R_{\Dmc,a}$ and $R_{\Dmc,b}$
of arity $n$, where $n$ is the number of individuals
in $\Dmc$. Then add $R_{\Dmc,a}(\vec{y})$ to
$\Kmc_{\Sigma,a}$ when constructing
$\varphi_{\Kmc,\Sigma,a}(x)$, where $\vec{y}$ is an enumeration
of the variables in $\Kmc_{\Sigma,a}$.
Do the same to construct $\varphi^{\text{GF}}_{\Kmc,\Sigma,b}(x)$,
using $R_{\Dmc,b}$ instead of $R_{\Dmc,a}$.
The formulas $\varphi^{\text{GF}}_{\Kmc,\Sigma,a}$ and $\neg\varphi^{\text{GF}}_{\Kmc,\Sigma,b}$ are in GF and play the same role
as the formulas $\varphi_{\Kmc,\Sigma,a}$ and $\varphi_{\Kmc,\Sigma,b}$. In particular, for any formula $\varphi$ the following are equivalent:

* $\varphi$ strongly $\Sigma$-separates $(\Kmc,\{a\},\{b\})$;

* $\varphi$ is an interpolant for $\varphi^{\text{GF}}_{\Kmc,\Sigma,a}(x),\neg \varphi^{\text{GF}}_{\Kmc,\Sigma,b}(x)$.

The complexity upper bound now follows from the result that interpolant existence in GF is decidable in 3[21].
For FO$^{2}$ we proceed as follows. We introduce for every individual name $c$
in $\Dmc$ a unary relation symbol $A_{c}$ and encode $\Dmc$ using the sentences
$\exists x A_{c}(x)\wedge \forall x\forall y (A_{c}(x) \wedge A_{c}(y) \rightarrow x=y)$,
for $c\in \text{ind}(\Dmc)$, and

* $\exists x \exists y R(x,y) \wedge A_c(x) \wedge A_{c'}(y)$ for every $R(c,c')\in \Dmc$;

* $\exists x A(x) \wedge A_c(x)$ for every $A(c)\in \Dmc$.

Let $\varphi^{2}_{\Kmc,\Sigma,a}$ be the conjunction of the sentences above, the sentences in $\Omc$, and the formula $A_{a}(x)$, where we also replace all relation symbols in $\Kmc$ that are not in $\Sigma$ by fresh relation symbols $R_{a}$.
Define $\varphi^{2}_{\Kmc,\Sigma,b}$ in the same way with $a$ replaced by $b$
and where the unary relation symbols $A_{c}'$ used to encode individuals $c$ are disjoint from the unary relation symbols used for this purpose in $\varphi^{2}_{\Kmc,\Sigma,a}$. Then we have that $\varphi^{2}_{\Kmc,\Sigma,a}$ and $\varphi^{2}_{\Kmc,\Sigma,b}$ are in FO$^{2}$ and a formula $\varphi$ strongly $\Sigma$-separates $(\Kmc,\{a\},\{b\})$ iff it is an interpolant for $\varphi_{\Kmc,\Sigma,a}^{2}(x),\neg \varphi_{\Kmc,\Sigma,b}^{2}(x)$.
The complexity upper bound now follows from the result that interpolant
non-existence in FO$^{2}$ is decidable in N[21].

The complexity lower bounds can be proved by generalizing in a straightforward way the reductions from interpolant existence to the existence of strongly separating formulas from the languages in $\DLS$ in the previous section to GF and FO$^{2}$ and using the complexity lower bounds for interpolant existence proved in [21].

there exists an $\mathcal{ALCO}$-forest model $\Amf$ of $\Kmc$ of finite
$\ALCO$-outdegree such that there exist an $n$ such that for all models $\Bmf$ of
$a\in P$: there exist $D\subseteq \text{dom}(\Bmf)$ of cardinality not
exceeding $n$ such that $a^{\Amf}\in D$ and the $\Sigma$-reduct of $\Amf_{|D}$ is $\mathcal{ALCO}$-rooted in $a^{\Bmf}$ and $\Bmf,a^{\Bmf}\not\rightarrow_{D,\mathcal{ALCO},\Sigma}
\Amf,b^{\Amf}$.