# Conservative Extensions in
Horn Description Logics with Inverse Roles

Jean Christoph Jung<EMAIL_ADDRESS>
Carsten Lutz<EMAIL_ADDRESS>
Mauricio Martel<EMAIL_ADDRESS>
Thomas Schneider<EMAIL_ADDRESS>
Fachbereich 3 Mathematik/Informatik
Universität Bremen
Postfach 330 440, 28334 Bremen, Germany

###### Abstract

We investigate the decidability and computational complexity of conservative
extensions and the related notions of inseparability and entailment in Horn
description logics (DLs) with inverse roles. We consider both query
conservative extensions, defined by requiring that the answers to all
conjunctive queries are left unchanged, and deductive conservative extensions,
which require that the entailed concept inclusions, role inclusions, and
functionality assertions do not change. Upper bounds for query conservative
extensions are particularly challenging because characterizations in terms of
unbounded homomorphisms between universal models, which are the foundation of
the standard approach to establishing decidability, fail in the presence of
inverse roles. We resort to a characterization that carefully mixes unbounded
and bounded homomorphisms and enables a decision procedure that combines tree
automata and a mosaic technique. Our main results are that query conservative
extensions are 2ExpTime-complete in all DLs between ${\cal E\\!\\!\>LI}$ and
Horn-${\cal ALCHIF}$ and between Horn-${\cal ALC}$ and Horn-${\cal ALCHIF}$,
and that deductive conservative extensions are 2ExpTime-complete in all DLs
between ${\cal E\\!\\!\>LI}$ and ${\cal E\\!\\!\>LHIF}_{\\!\\!\\!\>\bot}$. The
same results hold for inseparability and entailment.

##  1 Introduction

When accessing incomplete data, it can be beneficial to add an ontology
formulated in a decription logic (DL) to specify relevant domain knowledge, to
assign a semantics to the data, and to enrich and unify the vocabulary
available for querying. The resulting framework is known as ontology-mediated
querying (?, ?) and, in a data integration context, as ontology-based data
access, OBDA (?). Significant research activity on ontology-mediated query
evaluation has resulted in a thorough understanding of computational
complexity trade-offs and in various tools for evaluating queries in practice,
for a wide range of DLs such as DL-Lite (?, ?, ?), expressive Horn DLs such as
$\mathcal{ELI}$ and Horn-$\mathcal{SHIQ}$ (?, ?, ?, ?), and expressive “full
Boolean” DLs such as ${\cal ALC}$ and $\mathcal{SHIQ}$ (?, ?, ?, ?).

While query evaluation is by now rather well-understood, there is a need to
develop reasoning services that aim at engineering ontologies for ontology-
mediated querying and support tasks such as ontology versioning, ontology
import, and module extraction, which means to extract a subset from an
ontology that is sufficient for the application at hand (?, ?, ?). In all
these applications, it is important to relate different ontologies. In
versioning, for example, one would like to know whether replacing an ontology
with a new version has an effect on evaluating the relevant queries. In
ontology import, one wants to control the effect on query evaluation of
importing an existing ontology. And in module extraction, one wants to know
whether the module is really sufficient to evaluate the queries from the
application. All this can be formalized by requiring that when exchanging an
existing ontology with a new one, the answers to the relevant queries do not
change, over all possible data sets (?). One arrives at notions of
“equivalence” between ontologies that are different from logical equivalence.

We now make this more precise. In DLs, ontologies are represented as a _TBox_
while data sets are stored in an _ABox_. A _signature_ is a set of concept
names and role names. We say that a TBox
$\mathcal{T}_{2}\supseteq\mathcal{T}_{1}$ is an _$(\mathbf{A},\mathbf{Q})$
-query conservative extension_ of a TBox $\mathcal{T}_{1}$, where $\mathbf{A}$
and $\mathbf{Q}$ are signatures relevant for the data and queries,
respectively, if all $\mathbf{Q}$-queries give the same answers w.r.t.
$\mathcal{T}_{1}$ and w.r.t. $\mathcal{T}_{2}$, for every $\mathbf{A}$-ABox.
We thus identify the relevant queries by signature. Note that the subset
relationship $\mathcal{T}_{2}\supseteq\mathcal{T}_{1}$ is natural in some
applications such as ontology import and module extraction. It is not natural
in other applications such as versioning. In the general case, when
$\mathcal{T}_{1}$ need not be a subset of $\mathcal{T}_{2}$ and the above
condition is satisfied, we call $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$
_$(\mathbf{A},\mathbf{Q})$ -query inseparable_. We also consider the notion of
query entailment: $\mathcal{T}_{1}$ _$(\mathbf{A},\mathbf{Q})$ -query entails_
$\mathcal{T}_{2}$ if all $\mathbf{Q}$-queries give _at least_ the answers
w.r.t. $\mathcal{T}_{1}$ that they give w.r.t. $\mathcal{T}_{2}$, over every
$\mathbf{A}$-ABox. Clearly, query inseparability and conservative extensions
are special cases of query entailment: inseparability is bidirectional
entailment and conservative extensions are entailment under the promise that
$\mathcal{T}_{1}\subseteq\mathcal{T}_{2}$. When studying decidability or
computational complexity, it thus suffices to prove upper bounds for query
entailment and lower bounds for conservative extensions. For the query
language, we concentrate on conjunctive queries (CQs); since we work with Horn
DLs and quantify over the queries, this is equivalent to using unions of CQs
(UCQs) and positive existential queries (PEQs). Conservative extensions,
inseparability, query entailment of _TBoxes_ , as defined above, are useful
when knowledge is considered static and data changes frequently. Variants of
these notions for _knowledge bases (KBs)_ , which consist of a TBox and an
ABox, can be used for applications with static data (?, ?).

CQ entailment has been studied for various DLs (?, ?, ?, ?), also in the KB
version (?, ?), and also for OBDA specifications that involve mappings between
data sources and the ABox (?), see also the survey by ? (?). Nevertheless,
there is still a notable gap in our understanding of this notion: query
entailment between TBoxes is poorly understood in Horn DLs with inverse roles,
which are considered a crucial feature in many applications. There is in fact
a reason for this: as has already been observed by Botoeva et al. (?, ?),
standard techniques for Horn DLs without inverse roles fail when inverse roles
are added. More precisely, for Horn DLs without inverse roles query entailment
can be characterized by the existence of homomorphisms between universal
models (?, ?). The resulting characterizations provide an important foundation
for decision procedures, often based on tree automata emptiness (?). In the
presence of inverse roles, however, such characterizations are only correct if
one resorts to _bounded_ homomorphisms, that is, if one requires the existence
of an $n$-bounded homomorphism, _for any_ $n$ (?, ?). The unbounded $n$ in
$n$-bounded homomorphisms corresponds to CQs of unbounded size that can be
used for separating the two TBoxes. Unbounded homomorphisms, in contrast,
correspond to infinitary CQs, and while the (implicit) transition to
infinitary CQs poses no problems in DLs that do not admit inverse roles, it
compromises correctness in the presence of inverse roles. The ‘tighter’
characterization in terms of bounded homomorphism is problematic because it is
not obvious how the existence of such (infinite families of) homomorphisms can
be verified using tree automata or related techniques and, consequently,
decidability results for query conservative extensions in Horn DLs with
inverse roles are difficult to obtain. In fact, the only result of which we
are aware concerns inseparability _of KBs_ , and it is proved using intricate
game-theoretic techniques (?).

The aim of this article is to develop decision procedures for and study the
complexity of query conservative extensions, query inseparability, and query
entailment in Horn DLs with inverse roles such as ${\cal E\\!\\!\>LI}$ and
Horn-${\cal ALCHIF}$. The main idea for establishing decidability is to
provide a very careful characterization that mixes unbounded and bounded
homomorphisms, pushing the use of bounded homomorphisms to only those places
where they cannot possibly be avoided. We can then deal with the part of the
characterization that uses unbounded homomorphisms using tree automata while
the part that uses bounded homomorphisms is addressed up-front by precomputing
relevant information using a mosaic technique. In this way, we establish
decidability and a 2ExpTime upper bound for query entailment in the expressive
Horn DL Horn-${\cal ALCHIF}$, and thus also for query inseparability and query
conservative extensions. Together with known lower bounds (?), this yields
2ExpTime-completeness for all DLs between ${\cal E\\!\\!\>LI}$ and Horn-${\cal
ALCHIF}$ as well as between Horn-${\cal ALC}$ and Horn-${\cal ALCHIF}$. To be
more precise, the complexity is single exponential in the size of
$\mathcal{T}_{1}$ and double exponential only in the size of
$\mathcal{T}_{2}$.

We additionally study the _deductive_ version of query entailment, query
inseparability, and query conservative extensions. Here, instead of asking
whether the answers to all queries are preserved, the question is whether
$\mathcal{T}_{1}$ entails every concept inclusion, role inclusion, and
functionality assertion that $\mathcal{T}_{2}$ entails, over a given signature
$\mathbf{S}$. This problem, too, has received considerable interest in the
literature, but has not previously been studied for Horn DLs with inverse
roles. It is more appropriate than the query-based notions in applications
that require conceptual reasoning rather than querying data. It was
historically even the first notion of conservative extension studied for DLs
(?); we again refer to the survey (?) for a more detailed discussion. We show
that deductive entailment, deductive inseparability, and deductive
conservative extensions are 2ExpTime-complete for all DLs between ${\cal
E\\!\\!\>LI}$ and ${\cal E\\!\\!\>LHIF}_{\\!\\!\\!\>\bot}$; again, the runtime
of our algorithm is single exponential in the size of $\mathcal{T}_{1}$ and
double exponential in the size of $\mathcal{T}_{2}$. For the upper bound, we
first show that deductive entailment is essentially identical to query
entailment when the queries are tree-shaped CQs with a single answer variable.
We then characterize this version of query entailment using simulations in
place of homomorphisms; it is not necessary to resort to a bounded version of
simulations. This again enables a decision procedure based on tree automata
emptiness. The lower bound is proved by reduction from a certain homomorphism
problem between universal models for ABoxes w.r.t. ${\cal E\\!\\!\>LI}$
TBoxes, studied in the context of querying by example (?).

This article is structured as follows: in Section 2 we define the notions used
throughout the text; in Section 3 we establish the model-theoretic
characterizations; in Section 4 we develop the automata-based decision
procedure and prove the exact complexity for query entailment, inseparability,
and conservative extensions; Section 5 deals with the case of tree-shaped
queries and deductive query entailment; Section 6 discusses possible future
work. Proofs of some auxiliary lemmas can be found in the appendix.

##  2 Preliminaries

We define basic notions and lemmas that are needed in the remainder of the
article.

###  2.1 Description Logics

The main DL considered in this article is Horn-${\cal ALCHIF}$, a member of
the Horn-${\cal SHIQ}$ family of DLs whose reasoning problems have been widely
studied (?, ?, ?, ?, ?, ?). We introduce Horn-${\cal ALCHIF}$ and several of
its fragments. Let $\mathsf{N_{C}},\mathsf{N_{R}},\mathsf{N_{I}}$ be countably
infinite sets of _concept names_ , _role names_ , and _individual names_. A
_role_ is either a role name $r$ or an _inverse role_ $r^{-}$ where $r$ is a
role name. As usual, we identify $(r^{-})^{-}$ and $r$, allowing us to switch
between role names and their inverses easily. A _concept inclusion (CI)_ is of
the form $L\sqsubseteq R$, where $L$ and $R$ are concepts defined by the
syntax rules

$\displaystyle R,R^{\prime}$ $\displaystyle::=\top\mid\bot\mid A\mid\neg A\mid
R\sqcap R^{\prime}\mid\neg L\sqcup R\mid\exists r.R\mid\forall r.R$
$\displaystyle L,L^{\prime}$ $\displaystyle::=\top\mid\bot\mid A\mid L\sqcap
L^{\prime}\mid L\sqcup L^{\prime}\mid\exists r.L$

with $A$ ranging over concept names and $r$ over roles. A _role inclusion
(RI)_ is of the form $r\sqsubseteq s$ with $r,s$ roles, and a _functionality
assertion (FA)_ is of the form $\mathsf{func}(r)$ with $r$ a role. A _Horn-
${\cal ALCHIF}$ TBox_ $\mathcal{T}$ is a finite set of CIs, RIs, and FAs. To
avoid dealing with rather messy technicalities that do neither seem to be very
illuminating from a theoretical viewpoint nor too useful from a practical one,
we generally assume that functional roles cannot have subroles, that is,
$r\sqsubseteq s\in\mathcal{T}$ implies
$\mathsf{func}(s)\notin\mathcal{T}$.111Concerning the usefulness of allowing
functional roles to have subroles, we found that only 21 ($\leq{}$4.8%) out of
439 available ontologies in BioPortal (?) contain subroles of functional
roles; many of these occurrences appear to be due to modeling mistakes. We
conjecture that our main results also hold without that restriction.

In this article, we consider the following fragments of Horn-${\cal ALCHIF}$.
A _Horn- ${\cal ALC}$_ TBox $\mathcal{T}$ is a finite set of CIs that do not
use inverse roles. An _${\cal E\\!\\!\ >LI}_{\\!\\!\>\bot}$ concept_ is an
expression that is built according to the syntax rule for $L$ above, but does
not use “$\sqcup$”. An _${\cal E\\!\\!\ >LI}_{\\!\\!\>\bot}$ CI_ is a CI of
the form $L\sqsubseteq R$ where both $L$ and $R$ are ${\cal
E\\!\\!\>LI}_{\\!\\!\>\bot}$ concepts. An _${\cal E\\!\\!\
>LHIF}_{\\!\\!\\!\>\bot}$ TBox_ is a finite set of ${\cal
E\\!\\!\>LI}_{\\!\\!\>\bot}$ CIs, RIs, and FAs.

An _ABox_ $\mathcal{A}$ is a finite set of _concept and role assertions_ of
the form $A(a)$ and $r(a,b)$, where $A\in\mathsf{N_{C}}$, $r\in\mathsf{N_{R}}$
and $a,b\in\mathsf{N_{I}}$. We write $\mathsf{ind}(\mathcal{A})$ for the set
of individuals in $\mathcal{A}$. An ABox $\mathcal{A}$ is _tree-shaped_ if (i)
$\mathcal{A}$ does not contain an assertion of the form $r(a,a)$, (ii) the
undirected graph
$G_{\mathcal{A}}=(\mathsf{ind}(\mathcal{A}),\,\\{\\{a,b\\}\mid
r(a,b)\in\mathcal{A}\\})$ is a tree, and (iii) there are no multi-edges, that
is, for any $a,b\in\mathsf{ind}(\mathcal{A})$, $\mathcal{A}$ contains at most
one role assertion that involves both $a$ and $b$.

The semantics of Horn-${\cal ALCHIF}$ is defined in the usual way (?). An
_interpretation_ is a pair
$\mathcal{I}=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$, where
$\Delta^{\mathcal{I}}$ is a non-empty set, the _domain_ , and
$\cdot^{\mathcal{I}}$ is the _interpretation function_ , with
$A^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}$ for every $A\in\mathsf{N_{C}}$,
$r^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}$ for
every $r\in\mathsf{N_{R}}$, and $a^{\mathcal{I}}\in\Delta^{\mathcal{I}}$ for
every $a\in\mathsf{N_{I}}$. We make the standard name assumption, that is,
$a^{\mathcal{I}}=a$ for all $a\in\mathsf{N_{I}}$. The interpretation function
is extended to inverse roles and arbitrary concepts $C$ in the usual way:

$\begin{array}[]{@{}r@{~~}c@{~~}l@{\qquad}r@{~~}c@{~~}l@{\qquad}r@{~~}c@{~~}l@{}}(r^{-})^{\mathcal{I}}~{}~{}&=\hfil~{}~{}&\lx@intercol\\{(e,d)\mid(d,e)\in
<EMAIL_ADDRESS>\top^{\mathcal{I}}~{}~{}&=\hfil~{}~{}&\Delta^{\mathcal{I}}\\\\[2.0pt]
\bot^{\mathcal{I}}~{}~{}&=\hfil~{}~{}&\emptyset\\\\[2.0pt] (\lnot
C)^{\mathcal{I}}~{}~{}&=\hfil~{}~{}&\Delta^{\mathcal{I}}\setminus
C^{\mathcal{I}}\\\\[2.0pt] (C\sqcap
D)^{\mathcal{I}}~{}~{}&=\hfil~{}~{}&C^{\mathcal{I}}\cap
D^{\mathcal{I}}\\\\[2.0pt] (C\sqcup
D)^{\mathcal{I}}~{}~{}&=\hfil~{}~{}&C^{\mathcal{I}}\cup
D^{\mathcal{I}}\\\\[2.0pt] (\exists
r.C)^{\mathcal{I}}~{}~{}&=\hfil~{}~{}&\lx@intercol\\{d\mid\text{there
is~{}}e\in\Delta^{\mathcal{I}}\text{~{}with~{}}(d,e)\in
r^{\mathcal{I}}\text{~{}and~{}}e\in
<EMAIL_ADDRESS>(\forall
r.C)^{\mathcal{I}}~{}~{}&=\hfil~{}~{}&\lx@intercol\\{d\mid\text{for
all~{}}e\in\Delta^{\mathcal{I}},\text{~{}if~{}}(d,e)\in
r^{\mathcal{I}},\text{~{}then~{}}e\in
<EMAIL_ADDRESS>
An interpretation $\mathcal{I}$ satisfies

  * •

a CI $C\sqsubseteq D$, written $\mathcal{I}\models C\sqsubseteq D$, if
$C^{\mathcal{I}}\subseteq D^{\mathcal{I}}$;

  * •

an RI $r\sqsubseteq s$, written $\mathcal{I}\models r\sqsubseteq s$, if
$r^{\mathcal{I}}\subseteq s^{\mathcal{I}}$;

  * •

an FA $\mathsf{func}(r)$, written $\mathcal{I}\models\mathsf{func}(r)$, if
$r^{\mathcal{I}}$ is functional;

  * •

a concept assertion $A(a)$, written $\mathcal{I}\models A(a)$, if $a\in
A^{\mathcal{I}}$;

  * •

a role assertion $r(a,b)$, written $\mathcal{I}\models r(a,b)$, if $(a,b)\in
r^{\mathcal{I}}$.

$\mathcal{I}$ is a _model_ of a TBox $\mathcal{T}$, written
$\mathcal{I}\models\mathcal{T}$, if it satisfies all inclusions and assertions
in it, likewise for ABoxes. $\mathcal{A}$ is _consistent_ with $\mathcal{T}$
if $\mathcal{T}$ and $\mathcal{A}$ have a common model.

Tree-shaped interpretations are defined by analogy with tree-shaped ABoxes. We
additionally need a weaker variant that permits multi-edges: an interpretation
$\mathcal{I}$ is _weakly tree-shaped_ if there are no $d,r$ with $(d,d)\in
r^{\mathcal{I}}$ and the undirected graph
$(\Delta^{\mathcal{I}},\,\\{\\{d,e\\}\mid(d,e)\in r^{\mathcal{I}}\\})$ is a
tree. Thus, an interpretation $\mathcal{I}$ is _tree-shaped_ if it is weakly
tree-shaped and has no multi-edges, i.e., $r^{\mathcal{I}}\cap
s^{\mathcal{I}}=\emptyset$ for any two distinct roles $r,s$.

A _signature_ $\mathbf{S}$ is a set of concept and role names. An
_$\mathbf{S}$ -ABox_ is an ABox that uses only concept and role names from
$\mathbf{S}$, and _$\mathbf{S}$ -${\cal E\\!\\!\>LI}_{\\!\\!\>\bot}$ concepts_
and other syntactic objects are defined analogously.

Generally and without further notice, we work with Horn-${\cal ALCHIF}$ TBoxes
that are in a certain nesting-free _normal form_ , that is, they contain only
CIs of the form

$\top\sqsubseteq A\qquad A\sqsubseteq\bot\qquad A_{1}\sqcap A_{2}\sqsubseteq
B\qquad A\sqsubseteq\exists r.B\qquad A\sqsubseteq\forall r.B,$

where $A,B,A_{1},A_{2}$ are concept names and $r,s$ are roles. It is well-
known that every Horn-${\cal ALCHIF}$ TBox $\mathcal{T}$ can be converted into
a TBox $\mathcal{T}^{\prime}$ in normal form (introducing additional concept
names) such that $\mathcal{T}$ is a logical consequence of
$\mathcal{T}^{\prime}$ and every model of $\mathcal{T}$ can be extended to one
of $\mathcal{T}^{\prime}$ by interpreting the additional concept names (see,
e.g., ?). As a consequence, all results obtained in this article for TBoxes in
normal form lift to the general case. Note that a Horn-${\cal ALCHIF}$ TBox in
normal form is essentially an ${\cal E\\!\\!\>LI}_{\\!\\!\>\bot}$ TBox since
CIs of the form $A\sqsubseteq\forall r.B$ can be equivalently rewritten as
$\exists r^{-}.A\sqsubseteq B$.

###  2.2 Query Conservative Extensions and Entailment

A _conjunctive query (CQ)_ is of the form
$q(\mathbf{x})=\exists\mathbf{y}\,\varphi(\mathbf{x},\mathbf{y}),$ where
$\mathbf{x}$ and $\mathbf{y}$ are tuples of variables and
$\varphi(\mathbf{x},\mathbf{y})$ is a conjunction of _atoms_ of the form
$A(z)$ or $r(z,z^{\prime})$ with $A\in\mathsf{N_{C}}$, $r\in\mathsf{N_{R}}$,
and $z,z^{\prime}\in\mathbf{x}\cup\mathbf{y}$. We call $\mathbf{x}$ _answer
variables_ and $\mathbf{y}$ _quantified variables_ of $q$. Tree-shaped and
weakly tree-shaped CQs are defined by analogy with (weakly) tree-shaped ABoxes
and interpretations: a CQ $q$ is _weakly tree-shaped_ if it does not contain
atoms of the form $r(z,z)$ and the undirected graph
$(\mathbf{x}\cup\mathbf{y},~{}\\{\\{z,z^{\prime}\\}\mid
r(z,z^{\prime})\text{~{}is an atom in~{}}q\\})$ is a tree. A weakly tree-
shaped CQ $q$ is _tree-shaped_ or a _tCQ_ if $q$ has no multi-edges, that is,
for any two distinct variables $z,z^{\prime}$ in $q$, there is at most one
atom of the form $r(z,z^{\prime})$ or $r(z^{\prime},z)$ in $q$. A _1tCQ_ is a
tCQ with exactly one answer variable. We sometimes write
$r^{-}(z,z^{\prime})\in q$ to mean $r(z^{\prime},z)\in q$.

A _match_ of $q$ in an interpretation $\mathcal{I}$ is a function
$\pi:\mathbf{x}\cup\mathbf{y}\to\Delta^{\mathcal{I}}$ such that $\pi(z)\in
A^{\mathcal{I}}$ for every atom $A(z)$ of $q$ and $(\pi(z),\pi(z^{\prime}))\in
r^{\mathcal{I}}$ for every atom $r(z,z^{\prime})$ of $q$. We write
$\mathcal{I}\models q(a_{1},\dots,a_{n})$ if there is a match of $q$ in
$\mathcal{I}$ with $\pi(x_{i})=a_{i}$ for all $i<n$. A tuple $\mathbf{a}$ of
elements from $\mathsf{N_{I}}$ is a _certain answer_ to $q$ over an ABox
$\mathcal{A}$ given a TBox $\mathcal{T}$, written
$\mathcal{T},\mathcal{A}\models q(\mathbf{a})$, if $\mathcal{I}\models
q(\mathbf{a})$ for all models of $\mathcal{T}$ and $\mathcal{A}$.

###### Definition 1

Let $\mathbf{A},\mathbf{Q}$ be signatures and
$\mathcal{T}_{1},\mathcal{T}_{2}$ Horn-${\cal ALCHIF}$ TBoxes. We say that
_$\mathcal{T}_{1}$ $(\mathbf{A},\mathbf{Q})$-CQ entails $\mathcal{T}_{2}$_,
written
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\textup{CQ}}\mathcal{T}_{2}$,
if for all $\mathbf{A}$-ABoxes $\mathcal{A}$ consistent with $\mathcal{T}_{1}$
and $\mathcal{T}_{2}$, all $\mathbf{Q}$-CQs $q(\mathbf{x})$ and all tuples
$\mathbf{a}\subseteq\mathsf{ind}(\mathcal{A})$,
$\mathcal{T}_{2},\mathcal{A}\models q(\mathbf{a})$ implies
$\mathcal{T}_{1},\mathcal{A}\models q(\mathbf{a})$. If in addition
$\mathcal{T}_{1}\subseteq\mathcal{T}_{2}$, we say that _$\mathcal{T}_{2}$ is
an $(\mathbf{A},\mathbf{Q})$-CQ conservative extension of $\mathcal{T}_{1}$_.
If
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\textup{CQ}}\mathcal{T}_{2}$
and vice versa, then $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ are
_$(\mathbf{A},\mathbf{Q})$ -CQ inseparable_.

We also consider _$(\mathbf{A},\mathbf{Q})$ -1tCQ entailment_, denoted
$\models_{\mathbf{A},\mathbf{Q}}^{\textup{1tCQ}}$, _$(\mathbf{A},\mathbf{Q})$
-1tCQ conservative extensions_, and _$(\mathbf{A},\mathbf{Q})$ -1tCQ
inseparability_, defined in the obvious way by replacing CQs with 1tCQs.

If
$\mathcal{T}_{1}\not\models_{\mathbf{A},\mathbf{Q}}^{\text{CQ}}\mathcal{T}_{2}$
because $\mathcal{T}_{2},\mathcal{A}\models q(\mathbf{a})$ but
$\mathcal{T}_{1},\mathcal{A}\not\models q(\mathbf{a})$ for some
$\mathbf{A}$-ABox $\mathcal{A}$ consistent with both $\mathcal{T}_{i}$,
$\mathbf{Q}$-CQ $q(\mathbf{x})$ and tuple $\mathbf{a}$ over
$\mathsf{ind}(\mathcal{A})$, we call the triple $(\mathcal{A},q,\mathbf{a})$ a
_witness_ to non-entailment.

###### Example 2

Let
$\mathcal{T}_{1}=\\{\text{PhDStud}\sqsubseteq\exists\text{advBy}.\text{Prof},\text{adv}\sqsubseteq\text{advBy}^{-}\\}$
and $\mathcal{T}_{2}=\mathcal{T}_{1}\cup\\{\mathsf{func}(\text{advBy})\\}$,
$\mathbf{A}=\\{\text{PhDStud},\text{adv}\\}$ and
$\mathbf{Q}=\\{\text{Prof}\\}$. Then we have
$\mathcal{T}_{1}\not\models^{\textup{CQ}}_{\mathbf{A},\mathbf{Q}}\mathcal{T}_{2}$
because of the witness
$(\\{\text{PhDStud}(\text{john}),\text{adv}(\text{mary},\text{john})\\},\text{Prof}(x),\text{mary})$.

If we drop from Definition 1 the condition that $\mathcal{A}$ must be
consistent with both $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$, then we obtain
an alternative notion of CQ entailment that we call _CQ entailment with
inconsistent ABoxes_. While CQ entailment with inconsistent ABoxes trivially
implies CQ entailment in the original sense, the converse fails.

###### Example 3

Let $\mathcal{T}_{1}=\emptyset$, $\mathcal{T}_{2}=\\{A_{1}\sqcap
A_{2}\sqsubseteq\bot\\}$ and $\mathbf{A}=\\{A_{1},A_{2}\\}$,
$\mathbf{Q}=\\{B\\}$. Then
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\textup{CQ}}\mathcal{T}_{2}$
because none of the $\mathcal{T}_{i}$ uses the concept name $B$; however,
$\mathcal{T}_{1}$ does not $(\mathbf{A},\mathbf{Q})$-CQ entail
$\mathcal{T}_{2}$ with inconsistent ABoxes because of the witness
$(\\{A_{1}(a),A_{2}(a)\\},\,B(x),\,a)$.

The following lemma relates the two notions of CQ entailment. _CQ evaluation_
is the problem to decide, given a TBox $\mathcal{T}$, an ABox $\mathcal{A}$, a
CQ $q$, and a tuple $\mathbf{a}\in\mathsf{ind}(\mathcal{A})$, whether
$\mathcal{T},\mathcal{A}\models q(\mathbf{a})$.

###### Proposition 4

$(\mathbf{A},\mathbf{Q})$-CQ entailment with inconsistent ABoxes can be
decided in polynomial time given access to oracles deciding
$(\mathbf{A},\mathbf{Q})$-CQ entailment and CQ evaluation.

Consequently and since CQ evaluation is in ExpTime in Horn-${\cal ALCHIF}$
(?), all complexity results obtained in this article also apply to CQ
entailment with inconsistent ABoxes.

To prove Proposition 4, we introduce a notion of entailment that refers to the
(in)consistency of ABoxes: _$\mathcal{T}_{1}$ $\mathbf{A}$-inconsistency
entails $\mathcal{T}_{2}$_, written
$\mathcal{T}_{1}\models_{\mathbf{A}}^{\bot}\mathcal{T}_{2}$, if for all
$\mathbf{A}$-ABoxes $\mathcal{A}$: if $\mathcal{A}$ is inconsistent with
$\mathcal{T}_{2}$, then $\mathcal{A}$ is inconsistent with $\mathcal{T}_{1}$.
Also, given a TBox $\mathcal{T}$ and signatures $\mathbf{A},\mathbf{Q}$, we
say that $\mathcal{T}$ is _$(\mathbf{A},\mathbf{Q})$ -universal_ if
$\mathcal{T},\mathcal{A}\models q(\mathbf{a})$ for all $\mathbf{A}$-ABoxes
$\mathcal{A}$, $\mathbf{Q}$-CQs $q(\mathbf{x})$, and tuples $\mathbf{a}$ over
$\mathsf{ind}(\mathcal{A})$ that are of the same length as $\mathbf{x}$. The
following is proved in Appendix A.1.

###### Lemma 5

Let $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ be $\text{Horn-}{\cal{\cal
ALCHIF}}$ TBoxes and let $\mathbf{A},\mathbf{Q}$ be signatures. Then
$\mathcal{T}_{1}$ $(\mathbf{A},\mathbf{Q})$-CQ entails $\mathcal{T}_{2}$ with
inconsistent ABoxes iff one of the two following conditions holds.

  1. (1)

$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\textup{CQ}}\mathcal{T}_{2}$
and $\mathcal{T}_{1}\models_{\mathbf{A}}^{\bot}\mathcal{T}_{2}$;

  2. (2)

$\mathcal{T}_{1}$ is $(\mathbf{A},\mathbf{Q})$-universal.

Lemma 5 is the core ingredient to proving Proposition 4. We first note that
whether $\mathcal{T}_{1}$ is $(\mathbf{A},\mathbf{Q})$-universal can be
decided by polynomially many CQ evaluation checks. In fact, it is not hard to
verify that $\mathcal{T}_{1}$ is $(\mathbf{A},\mathbf{Q})$-universal iff
$\mathbf{Q}$ contains no role names222If there is an $r\in\mathbf{Q}$, then
any disconnected ABox $\mathcal{A}$ witnesses that $\mathcal{T}_{1}$ is not
$(\mathbf{A},\mathbf{Q})$-universal since
$\mathcal{T}_{1},\mathcal{A}\not\models r(a,b)$ whenever $a$ and $b$ are from
different maximal connected components of $\mathcal{A}$. and
$\mathcal{T}_{1},\mathcal{A}\models B(a)$ for all $\mathbf{A}$-ABoxes
$\mathcal{A}$ that contain a single assertion, all $\mathbf{Q}$-CQs $B(x)$,
and all $a\in\mathsf{ind}(\mathcal{A})$. Moreover,
$\mathcal{T}_{1}\models_{\mathbf{A}}^{\bot}\mathcal{T}_{2}$ iff the following
conditions are satisfied:

  1. 1.

$\mathcal{T}_{1}^{A}\models_{\mathbf{A},\\{A\\}}^{\textup{CQ}}\mathcal{T}_{2}^{A}$,
where $A$ is a fresh concept name and $\mathcal{T}_{i}^{A}$ is obtained from
$\mathcal{T}_{i}$ by replacing each occurrence of $\bot$ with $A$ and adding
the axioms $A\sqsubseteq\forall s.A$ and $A\sqsubseteq\forall s^{-}.A$ for
every role $s$ that occurs in $\mathcal{T}_{i}$, for $i=1,2$;

  2. 2.

every $\mathbf{A}$-ABox $\mathcal{A}=\\{r(a,b),r(a,c)\\}$ inconsistent with
$\mathcal{T}_{2}$ is also inconsistent with $\mathcal{T}_{1}$.

This is proved in detail in Appendix A.2. In summary, we obtain Proposition 4.

We close this section with a general remark on the impact of role inclusions
on $(\mathbf{A},\mathbf{Q})$-entailment. It is easy to see that
$\mathcal{T}_{1}\not\models_{\mathbf{A},\mathbf{Q}}^{\textup{CQ}}\mathcal{T}_{2}$
if there is an $\mathbf{A}$-role $r$ and a $\mathbf{Q}$-role $s$ with
$\mathcal{T}_{2}\models r\sqsubseteq s$ but $\mathcal{T}_{1}\not\models
r\sqsubseteq s$. We write
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\text{RI}}\mathcal{T}_{2}$ if
there are no such $r$ and $s$. Clearly,
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\text{RI}}\mathcal{T}_{2}$
can be decided in exponential time: for all
$\mathcal{O}(|\mathbf{A}|\cdot|\mathbf{Q}|)$ many pairs of roles, subsumption
w.r.t. both $\mathcal{T}_{i}$ needs to be tested, and each such test can be
reduced to concept subsumption (?), which is in ExpTime for the extension
${\cal SHIQ}$ of $\text{Horn-}{\cal{\cal ALCHIF}}$ (?). It is thus safe to
assume
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\text{RI}}\mathcal{T}_{2}$
when deciding CQ entailment, which we will generally do from now on to avoid
dealing with special cases.

###  2.3 Deductive Conservative Extensions

Another natural notion of entailment that has received significant attention
in the literature is deductive entailment, which generalizes the notion of
deductive conservative extensions, and which separates two TBoxes in terms of
concept and role inclusions and functionality assertions, instead of ABoxes
and queries (?, ?, ?, ?).

###### Definition 6

Let $\mathbf{S}$ be a signature and let $\mathcal{T}_{1}$ and
$\mathcal{T}_{2}$ be ${\cal E\\!\\!\>LHIF}_{\\!\\!\\!\>\bot}$ TBoxes. We say
that _$\mathcal{T}_{1}$ $\mathbf{S}$-deductively entails $\mathcal{T}_{2}$_,
written $\mathcal{T}_{1}\models_{\mathbf{S}}^{\textup{TBox}}\mathcal{T}_{2}$,
if for all $\mathbf{S}$-${\cal E\\!\\!\>LI}_{\\!\\!\>\bot}$-concept inclusions
$\alpha$ and all $\mathbf{S}$-RIs and $\mathbf{S}$-FAs $\alpha$:
$\mathcal{T}_{2}\models\alpha$ implies $\mathcal{T}_{1}\models\alpha$. If
additionally $\mathcal{T}_{1}\subseteq\mathcal{T}_{2}$, then we say that
_$\mathcal{T}_{2}$ is an $\mathbf{S}$-deductive conservative extension of
$\mathcal{T}_{1}$_. If
$\mathcal{T}_{1}\models_{\mathbf{S}}^{\textup{TBox}}\mathcal{T}_{2}$ and vice
versa, then $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ are _$\mathbf{S}$
-deductively inseparable_.

Deductive conservative extensions in other DLs is defined accordingly, that
is, separation takes place in terms of the TBox statements that are admitted
in the DL under consideration. In contrast to $(\mathbf{A},\mathbf{Q})$-query
entailment, only one signature is relevant for $\mathbf{S}$-deductive
entailment (unless one would want to distinguish the signatures of the two
sides in CIs or RIs, which seems unintuitive). Although $\mathbf{S}$-deductive
entailment and $(\mathbf{S},\mathbf{S})$-query entailment are closely related,
it is not difficult to see that they are orthogonal.

###### Example 7

Let $\mathcal{T}_{1}$, $\mathcal{T}_{2}$ be as in Example 3 and
$\mathbf{S}=\\{A_{1},A_{2},B\\}$. Then
$\mathcal{T}_{1}\not\models_{\mathbf{S}}^{\textup{TBox}}\mathcal{T}_{2}$,
witnessed by the ${\cal E\\!\\!\>LI}$ CI $A_{1}\sqcap A_{2}\sqsubseteq B$.
However,
$\mathcal{T}_{1}\models_{\mathbf{S},\mathbf{S}}^{\textup{CQ}}\mathcal{T}_{2}$
because $\mathbf{S}$-CQs cannot detect the disjointness of $A_{1}$ and $A_{2}$
based on ABoxes that are consistent with $\mathcal{T}_{2}$.

For the converse direction, let $\mathcal{T}_{1}=\emptyset$ and
$\mathcal{T}_{2}=\\{A\sqsubseteq\exists r.B\\}$, and $\mathbf{S}=\\{A,B\\}$.
Then
$\mathcal{T}_{1}\not\models_{\mathbf{S},\mathbf{S}}^{\textup{CQ}}\mathcal{T}_{2}$
is witnessed by $(\\{A(a)\\},\exists x\,B(x),a)$. However, since ${\cal
E\\!\\!\>LI}_{\\!\\!\>\bot}$ CIs cannot jump to an unreachable point like the
existential quantifier in the CQ $\exists x\,B(x)$, we have
$\mathcal{T}_{1}\models_{\mathbf{S}}^{\textup{TBox}}\mathcal{T}_{2}$.

For $\mathbf{S}$-deductive entailment and $(\mathbf{S},\mathbf{S})$-_1tCQ_
entailment, the connection is even more intimate. In fact, we have the
following.

###### Proposition 8

In ${\cal E\\!\\!\>LHIF}_{\\!\\!\\!\>\bot}$, $\mathbf{S}$-deductive entailment
can be decided in polynomial time given access to oracles for
$(\mathbf{S},\mathbf{S})$-1tCQ entailment and 1tCQ evaluation.

In fact, Proposition 8 is a consequence of the following lemma and the
observations about $\mathcal{T}_{1}\models_{\mathbf{S}}^{\bot}\mathcal{T}_{2}$
made in Section 2.2. A proof is in Appendix A.3.

###### Lemma 9

Let $\mathbf{S}$ be a signature and $\mathcal{T}_{1},\mathcal{T}_{2}$ ${\cal
E\\!\\!\>LHIF}_{\\!\\!\\!\>\bot}$ TBoxes such that
$\mathcal{T}_{1}\models_{\mathbf{S},\mathbf{S}}^{\textup{RI}}\mathcal{T}_{2}$.
Then

$\mathcal{T}_{1}\models_{\mathbf{S}}^{\textup{TBox}}\mathcal{T}_{2}\quad\text{iff}\quad\mathcal{T}_{1}\models_{\mathbf{S},\mathbf{S}}^{\textup{1tCQ}}\mathcal{T}_{2}\quad\text{and}\quad\mathcal{T}_{1}\models_{\mathbf{S}}^{\bot}\mathcal{T}_{2}.$

Note that Definition 6 assumes the TBoxes $\mathcal{T}_{1}$ and
$\mathcal{T}_{2}$ to be formulated in ${\cal E\\!\\!\>LHIF}_{\\!\\!\\!\>\bot}$
rather than in $\text{Horn-}{\cal{\cal ALCHIF}}$. This is because the main
theme of this article are query conservative extensions and, as demonstrated
by Proposition 8, separation in terms of ${\cal E\\!\\!\>LI}_{\\!\\!\>\bot}$
concept inclusions is closely related to separation by (tree-shaped) ABoxes
and 1tCQs. Now, separation in terms of ${\cal E\\!\\!\>LI}_{\\!\\!\>\bot}$
concept inclusions is the natural choice for ${\cal
E\\!\\!\>LHIF}_{\\!\\!\\!\>\bot}$ TBoxes as ${\cal
E\\!\\!\>LHIF}_{\\!\\!\\!\>\bot}$ is based on the concept language ${\cal
E\\!\\!\>LI}_{\\!\\!\>\bot}$ while this is not true for
$\text{Horn-}{\cal{\cal ALCHIF}}$. All results in this article that concern
deductive conservative extensions (and related notions) actually remain valid
also when $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ are $\text{Horn-}{\cal{\cal
ALCHIF}}$ TBoxes, while separation is still in terms of ${\cal
E\\!\\!\>LI}_{\\!\\!\>\bot}$ CIs. Separating $\text{Horn-}{\cal{\cal ALCHIF}}$
TBoxes in terms of $\text{Horn-}{\cal{\cal ALCHIF}}$ is an interesting topic
that is outside the scope of this article, see Section 6 for some additional
discussion.

###  2.4 Homomorphisms and Simulations

Homomorphisms, both in their (standard) unbounded form and in bounded form,
are an elementary tool for dealing with CQs. Likewise, (unbounded) simulations
are closely linked to 1tCQs. We will make extensive use of these notions
throughout the article.

For interpretations $\mathcal{I}_{1},\mathcal{I}_{2}$ and a signature
$\mathbf{S}$, an _$\mathbf{S}$ -homomorphism_ from $\mathcal{I}_{1}$ to
$\mathcal{I}_{2}$ is a total function
$h:\Delta^{\mathcal{I}_{1}}\to\Delta^{\mathcal{I}_{2}}$ that satisfies the
following conditions.

  1. (1)

$h(a)=a$ for all $a\in\mathsf{N_{I}}$;

  2. (2)

$h(d)\in A^{\mathcal{I}_{2}}$ for all $d\in A^{\mathcal{I}_{1}}$,
$A\in\mathsf{N_{C}}\cap\mathbf{S}$;

  3. (3)

$(h(d),h(d^{\prime}))\in r^{\mathcal{I}_{2}}$ for all $(d,d^{\prime})\in
r^{\mathcal{I}_{1}}$, $r\in\mathsf{N_{R}}\cap\mathbf{S}$.

We write $\mathcal{I}_{1}\to_{\mathbf{S}}\mathcal{I}_{2}$ to denote the
existence of an $\mathbf{S}$-homomorphism from $\mathcal{I}_{1}$ to
$\mathcal{I}_{2}$. If $\mathbf{S}=\mathsf{N_{C}}\cup\mathsf{N_{R}}$, we write
$\mathcal{I}\to\mathcal{J}$.

Let $\mathcal{I}_{1},\mathcal{I}_{2}$ be interpretations,
$d\in\Delta^{\mathcal{I}_{1}}$, and $n\geq 0$. We say that there is an _$n$
-bounded $\mathbf{S}$-homomorphism_ from $\mathcal{I}_{1}$ to
$\mathcal{I}_{2}$, written
$\mathcal{I}_{1}\rightarrow^{n}_{\mathbf{S}}\mathcal{I}_{2}$, if for any
subinterpretation333We mean an interpretation $\mathcal{I}^{\prime}_{1}$ such
that $\Delta^{\mathcal{I}^{\prime}_{1}}\subseteq\Delta^{\mathcal{I}}$,
$A^{\mathcal{I}^{\prime}_{1}}=A^{\mathcal{I}}\cap\Delta^{\mathcal{I}^{\prime}_{1}}$
for all concept names $A$, and
$r^{\mathcal{I}^{\prime}_{1}}=r^{\mathcal{I}}\cap(\Delta^{\mathcal{I}^{\prime}_{1}}\times\Delta^{\mathcal{I}^{\prime}_{1}})$
for all role names $r$. $\mathcal{I}^{\prime}_{1}$ of $\mathcal{I}_{1}$ with
$|\Delta^{\mathcal{I}^{\prime}_{1}}|\leq n$, we have
$\mathcal{I}^{\prime}_{1}\rightarrow_{\mathbf{S}}\mathcal{I}_{2}$. Moreover,
we write
$\mathcal{I}_{1}\rightarrow^{\mathsf{fin}}_{\mathbf{S}}\mathcal{I}_{2}$ if
$\mathcal{I}_{1}\rightarrow^{n}_{\mathbf{S}}\mathcal{I}_{2}$ for every $n$. If
$\mathbf{S}=\mathsf{N_{C}}\cup\mathsf{N_{R}}$, we write
$\mathcal{I}\to^{\mathsf{fin}}\mathcal{J}$.

For $d\in\Delta^{\mathcal{I}}$ and $n\geq 0$, we denote with
$\mathcal{I}|^{d}_{n}$ the restriction of interpretation $\mathcal{I}$ to
elements that can be reached by starting at $d$ and traveling along at most
$n$ role edges (forwards or backwards). The following is standard to prove.

###### Lemma 10

Let $\mathbf{S}$ be a signature and $\mathcal{I}_{1},\mathcal{I}_{2}$ be
interpretations.

  1. 1.

If $\mathcal{I}_{1}\rightarrow_{\mathbf{S}}\mathcal{I}_{2}$, then for all
$\mathbf{S}$-CQs $q$ and tuples $\mathbf{a}$, $\mathcal{I}_{1}\models
q(\mathbf{a})$ implies $\mathcal{I}_{2}\models q(\mathbf{a})$.

  2. 2.

For every $n\geq 0$, if
$\mathcal{I}_{1}\rightarrow_{\mathbf{S}}^{n}\mathcal{I}_{2}$, then for all
$\mathbf{S}$-CQs $q$ with at most $n$ variables and all tuples $\mathbf{a}$,
$\mathcal{I}_{1}\models q(\mathbf{a})$ implies $\mathcal{I}_{2}\models
q(\mathbf{a})$.

  3. 3.

If $\mathcal{I}_{1}$ is finitely branching, then the following are equivalent:

    1. (a)

$\mathcal{I}_{1}\rightarrow_{\mathbf{S}}^{\mathsf{fin}}\mathcal{I}_{2}$;

    2. (b)

$\mathcal{I}_{1}|^{d}_{i}\rightarrow_{\mathbf{S}}\mathcal{I}_{2}$ for every
$d\in\Delta^{\mathcal{I}_{1}}$ and $i\geq 0$.

Given a signature $\mathbf{S}$ and two interpretations
$\mathcal{I},\mathcal{J}$, an _$\mathbf{S}$ -simulation of $\mathcal{I}$ in
$\mathcal{J}$_ is a relation
$\sigma\subseteq\Delta^{\mathcal{I}}\times\Delta^{\mathcal{J}}$ that satisfies
the following conditions.

  * (1)

$(a,a)\in\sigma$ for all $a\in\mathsf{N_{I}}$;

  * (2)

if $d\in A^{\mathcal{I}}$ with $A\in\mathbf{S}$ and $(d,e)\in\sigma$, then
$e\in A^{\mathcal{J}}$;

  * (3)

if $(d,d^{\prime})\in r^{\mathcal{I}}$ with $r$ an $\mathbf{S}$-role and
$(d,e)\in\sigma$, then there is some $e^{\prime}$ with $(e,e^{\prime})\in
r^{\mathcal{J}}$ and $(d^{\prime},e^{\prime})\in\sigma$.

We write $\mathcal{I}\preceq_{\mathbf{S}}\mathcal{J}$ if there is an
$\mathbf{S}$-simulation of $\mathcal{I}$ in $\mathcal{J}$. Point 1 of Lemma 10
still holds when homomorphisms are replaced with simulations and CQs with
1tCQs.

###  2.5 The Universal Model

We next introduce universal models, whose existence is a distinguishing
feature of Horn logics. More precisely, for every $\text{Horn-}{\cal{\cal
ALCHIF}}$ TBox $\mathcal{T}$ and ABox $\mathcal{A}$, there is a model
$\mathcal{I}_{\mathcal{T},\mathcal{A}}$ of $\mathcal{T}$ and $\mathcal{A}$
that homomorphically embeds into every model of $\mathcal{T}$ and
$\mathcal{A}$. This last property, together with Point 1 of Lemma 10, ensures
that $\mathcal{I}_{\mathcal{T},\mathcal{A}}$ is universal in the sense that
the certain answers to any CQ $q$ over $\mathcal{A}$ given $\mathcal{T}$ can
be obtained by evaluating $q$ over $\mathcal{I}_{\mathcal{T},\mathcal{A}}$. We
define the universal model by extending the ABox in a forward chaining way
akin to the chase in database theory.

Let $\mathcal{T}$ be a $\text{Horn-}{\cal{\cal ALCHIF}}$ TBox in normal form
and $\mathcal{A}$ an ABox that is consistent with $\mathcal{T}$. For a set $t$
of concept names, we write $\bigsqcap t$ as a shorthand for $\bigsqcap_{A\in
t}A$. A $\mathcal{T}$-_type_ is a set $t$ of concept names that occur in
$\mathcal{T}$ such that $\mathcal{T}\models\bigsqcap t\sqsubseteq A$ implies
$A\in t$ for all concept names $A$. For $a\in\mathsf{ind}(\mathcal{A})$ and
with $\mathcal{T}$ understood, let $\mathsf{tp}_{\mathcal{T}}(a)$ denote the
$\mathcal{T}$-type $\\{A\mid\mathcal{T},\mathcal{A}\models A(a)\\}$. When
$t,t^{\prime}$ are $\mathcal{T}$-types, $r$ is a role, and
$a\in\mathsf{ind}(\mathcal{A})$, we write

  * •

$t\rightsquigarrow^{\mathcal{T}}_{r}t^{\prime}$ if
$\mathcal{T}\models\bigsqcap t\sqsubseteq\exists r.\bigsqcap t^{\prime}$ and
$t^{\prime}$ is maximal with this condition;

  * •

$a\rightsquigarrow^{\mathcal{T},\mathcal{A}}_{r}t$ if
$\mathcal{T},\mathcal{A}\models\exists r.\bigsqcap t(a)$ and $t$ is maximal
with this condition.

The relations $\rightsquigarrow^{\mathcal{T}}_{r}$ and
$\rightsquigarrow_{r}^{\mathcal{T},\mathcal{A}}$ can be computed in
exponential time: for every $t,t^{\prime}$ (resp. $a,t$), the above entailment
test requires at most exponential time since subsumption (resp. instance
checking) in ${\cal SHIQ}$ is ExpTime-complete (?). A _path for $\mathcal{A}$
and $\mathcal{T}$_ is a finite sequence
$\pi=ar_{0}t_{1}\cdots\linebreak[2]t_{n-1}r_{n-1}t_{n}$, $n\geq 0$, with
$a\in\mathsf{ind}(\mathcal{A})$, $r_{0},\dots,r_{n-1}$ roles, and
$t_{1},\dots,t_{n}$ $\mathcal{T}$-types such that

  1. (i)

$a\rightsquigarrow^{\mathcal{T},\mathcal{A}}_{r_{0}}t_{1}$ and, if
$\mathsf{func}(r_{0})\in\mathcal{T}$, then there is no
$b\in\mathsf{ind}(\mathcal{A})$ such that $\mathcal{T},\mathcal{A}\models
r_{0}(a,b)$;

  2. (ii)

$t_{i}\rightsquigarrow^{\mathcal{T}}_{r_{i}}t_{i+1}$ and, if
$\mathsf{func}(r_{i})\in\mathcal{T}$, then $r_{i-1}\neq r_{i}^{-}$, for $1\leq
i<n$.

When $n>0$, we use $\mathsf{tail}(\pi)$ to denote $t_{n}$. Let
$\mathsf{Paths}$ be the set of all paths for $\mathcal{A}$ and $\mathcal{T}$.
The _universal model_ $\mathcal{I}_{\mathcal{T},\mathcal{A}}$ of $\mathcal{T}$
and $\mathcal{A}$ is defined as follows:

$\displaystyle\Delta^{\mathcal{I}_{\mathcal{T},\mathcal{A}}}$
$\displaystyle=\mathsf{Paths}$ $\displaystyle
A^{\mathcal{I}_{\mathcal{T},\mathcal{A}}}$
$\displaystyle=\\{a\in\mathsf{ind}(\mathcal{A})\mid\mathcal{T},\mathcal{A}\models
A(a)\\}\;\cup\;\\{\pi\in\Delta^{\mathcal{I}}\setminus\mathsf{ind}(\mathcal{A})\mid\mathcal{T}\models\bigsqcap\mathsf{tail}(\pi)\sqsubseteq
A\\}$ $\displaystyle r^{\mathcal{I}_{\mathcal{T},\mathcal{A}}}$
$\displaystyle=\\{(a,b)\in\mathsf{ind}(\mathcal{A})\times\mathsf{ind}(\mathcal{A})\mid
s(a,b)\in\mathcal{A}\text{~{}and~{}}\mathcal{T}\models s\sqsubseteq
r\\}\;\cup$ $\displaystyle\phantom{{}={}}\\{(\pi,\pi st)\mid\pi
st\in\mathsf{Paths}\text{~{}and~{}}\mathcal{T}\models s\sqsubseteq r\\}\;\cup$
$\displaystyle\phantom{{}={}}\\{(\pi st,\pi)\mid\pi
st\in\mathsf{Paths}\text{~{}and~{}}\mathcal{T}\models s^{-}\sqsubseteq r\\}.$

We also need a universal model $\mathcal{I}_{\mathcal{T},t}$ of a TBox
$\mathcal{T}$ and a type $t$, instead of an ABox. More precisely, we define
$\mathcal{I}_{\mathcal{T},t}=\mathcal{I}_{\mathcal{T},\mathcal{A}_{t}}$ where
$\mathcal{A}_{t}=\\{A(a)\mid A\in t\\}$ for a fixed $a\in\mathsf{N_{I}}$.

The following lemma summarizes the main properties of universal models. The
proof is standard and omitted (see, e.g., ?).

###### Lemma 11

For every $\text{Horn-}{\cal{\cal ALCHIF}}$ TBox $\mathcal{T}$ in normal form
and ABox $\mathcal{A}$ consistent with $\mathcal{T}$, the following hold:

  1. (1)

$\mathcal{I}_{\mathcal{T},\mathcal{A}}$ is a model of $\mathcal{T}$ and
$\mathcal{A}$;

  2. (2)

$\mathcal{I}_{\mathcal{T},\mathcal{A}}\rightarrow\mathcal{I}$ for all models
$\mathcal{I}$ of $\mathcal{T}$ and $\mathcal{A}$;

  3. (3)

$\mathcal{T},\mathcal{A}\models q(\mathbf{a})$ iff
$\mathcal{I}_{\mathcal{T},\mathcal{A}}\models q(\mathbf{a})$, for all CQs
$q(\mathbf{x})$ and tuples $\mathbf{a}$ of individuals;

  4. (4)

$\mathcal{I}_{\mathcal{T},t}\to\mathcal{I}_{\mathcal{T},t^{\prime}}$ for all
$\mathcal{T}$-types $t,t^{\prime}$ with $t\subseteq t^{\prime}$.

We shall sometimes refer to subinterpretations of universal models. Given a
TBox $\mathcal{T}$, an ABox $\mathcal{A}$, and
$a\in\mathsf{ind}(\mathcal{A})$, we use
$\mathcal{I}_{\mathcal{T},\mathcal{A}}|_{a}$ to denote the subinterpretation
of $\mathcal{I}_{\mathcal{T},\mathcal{A}}$ rooted at $a$, i.e., the
restriction of $\mathcal{I}_{\mathcal{T},\mathcal{A}}$ to all paths $\pi$
beginning with $a$. Clearly, $\mathcal{I}_{\mathcal{T},\mathcal{A}}|_{a}$ is
weakly tree-shaped.

##  3 Model-Theoretic Characterization

We aim to provide a model-theoretic characterization of CQ-entailment that
will be the basis for our decision procedure later on. We proceed in two
steps. We first show that non-entailment between $\mathcal{T}_{1}$ and
$\mathcal{T}_{2}$ is always witnessed by a tree-shaped ABox and a weakly tree-
shaped CQ with at most one answer variable. Second, we provide the desired
characterization, using a careful mix of bounded and unbounded homomorphisms.
We also establish a version for 1tCQ-entailment that uses (unbounded)
simulations.

###  3.1 Tree-Shaped Witnesses

We show that non-entailment between $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ is
always witnessed by a tree-shaped ABox and a weakly tree-shaped CQ with at
most one answer variable. The idea is to first manipulate the witnessing CQ so
that it takes the desired form and to then unravel the ABox.

We start with defining ABox unraveling (see also ?). The _unraveling_
$U_{\mathcal{A}}^{a}$ of an ABox $\mathcal{A}$ at an individual
$a\in\mathsf{ind}(\mathcal{A})$ is the following (usually infinite) ABox:

  * •

$\mathsf{ind}(U_{\mathcal{A}}^{a})$ is the set of sequences
$b_{0}r_{0}b_{1}\cdots r_{n-1}b_{n}$ with $n\geq 0$, where $b_{0}=a$,
$b_{i}\in\mathsf{ind}(\mathcal{A})$ for all $0\leq i\leq n$,
$r_{i}(b_{i},b_{i+1})\in\mathcal{A}$ for all $0\leq i<n$, and
$(b_{i-1},r^{-}_{i-1})\neq(b_{i+1},r_{i})$ (the latter inequality is needed to
ensure preservation of functionality);

  * •

the concept assertions in $U_{\mathcal{A}}^{a}$ are all assertions of the
shape $C(\alpha)$ such that $\alpha=b_{0}\cdots
b_{n}\in\mathsf{ind}(U_{\mathcal{A}}^{a})$ and $C(b_{n})\in\mathcal{A}$, and
the role assertions in $U_{\mathcal{A}}^{a}$ are all assertions of the shape
$r(b_{0}\cdots b_{n-1},\alpha)$ such that $\alpha=b_{0}\cdots
b_{n-1}rb_{n}\in\mathsf{ind}(U_{\mathcal{A}}^{a})$.

The following is not hard to prove (see ?).

###### Lemma 12

Let $\mathcal{T}$ be a $\text{Horn-}{\cal{\cal ALCHIF}}$ TBox, $\mathcal{A}$
an ABox that is consistent with $\mathcal{T}$, and
$a\in\mathsf{ind}(\mathcal{A})$. Then

  1. (a)

$U_{\mathcal{A}}^{a}$ is consistent with $\mathcal{T}$;

  2. (b)

$\mathcal{I}_{\mathcal{T},U_{\mathcal{A}}^{a}}\to\mathcal{I}_{\mathcal{T},\mathcal{A}}$;

  3. (c)

$\mathcal{I}_{\mathcal{T},U_{\mathcal{A}}^{a}}|_{a}$ is isomorphic to
$\mathcal{I}_{\mathcal{T},\mathcal{A}}|_{a}$.

We now prove the main result of this section.

###### Proposition 13

Let $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ be $\text{Horn-}{\cal{\cal
ALCHIF}}$ TBoxes with
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\textup{RI}}\mathcal{T}_{2}$.
If
$\mathcal{T}_{1}\not\models_{\mathbf{A},\mathbf{Q}}^{\textup{CQ}}\mathcal{T}_{2}$,
then there is a witness $(\mathcal{A},q,\mathbf{a})$ where $\mathcal{A}$ is
tree-shaped and $q$ is weakly tree-shaped and has at most one answer variable.

Proof.  Assume
$\mathcal{T}_{1}\not\models_{\mathbf{A},\mathbf{Q}}^{\text{CQ}}\mathcal{T}_{2}$,
i.e., $\mathcal{T}_{2},\mathcal{A}\models q(\mathbf{a})$ and
$\mathcal{T}_{1},\mathcal{A}\not\models q(\mathbf{a})$, for some
$\mathbf{A}$-ABox $\mathcal{A}$ consistent with both $\mathcal{T}_{i}$, some
$\mathbf{Q}$-CQ $q(\mathbf{x})$ and some tuple $\mathbf{a}$. Lemma 11 (3)
yields $\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\models q(\mathbf{a})$ and
$\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}\not\models q(\mathbf{a})$. We first
show that the following properties of $q$ and $\mathbf{a}$ are without loss of
generality.

  1. (a)

Every match $\pi$ of $q(\mathbf{x})$ in
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ with $\pi(\mathbf{x})=\mathbf{a}$
maps every quantified variable into the anonymous part;

  2. (b)

every match $\pi$ of $q(\mathbf{x})$ in
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ with $\pi(\mathbf{x})=\mathbf{a}$
maps the quantified variables to pairwise distinct elements;

  3. (c)

$q(\mathbf{x})$ does not contain atoms of the form $r(x_{1},x_{2})$ with
$x_{1},x_{2}$ answer variables;

  4. (d)

$q(\mathbf{x})$ is connected.

_For ( a)_, take a match $\pi$ of $q$ in
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ with $\pi(\mathbf{x})=\mathbf{a}$.
If there is a quantified variable $y$ such that
$\pi(y)=b\in\mathsf{ind}(\mathcal{A})$, obtain $q^{\prime}(\mathbf{x},y)$ from
$q(\mathbf{x})$ by removing the quantification over $y$, thus making $y$ an
answer variable. Clearly, we have
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\models q^{\prime}(\mathbf{a},b)$
and $\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}\not\models
q^{\prime}(\mathbf{a},b)$, and thus $\mathcal{T}_{2},\mathcal{A}\models
q^{\prime}(\mathbf{a},b)$ and $\mathcal{T}_{1},\mathcal{A}\not\models
q^{\prime}(\mathbf{a},b)$.

_For ( b)_, take a match $\pi$ of $q$ in
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ with $\pi(\mathbf{x})=\mathbf{a}$.
If there are quantified variables $y,y^{\prime}$ such that $y\neq y^{\prime}$
and $\pi(y)=\pi(y^{\prime})$, obtain $q^{\prime}(\mathbf{x})$ from
$q(\mathbf{x})$ by replacing all occurrences of $y^{\prime}$ with $y$ and
removing quantification over $y^{\prime}$. Clearly, we have
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\models q^{\prime}(\mathbf{a})$ and
$\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}\not\models q^{\prime}(\mathbf{a})$,
and thus $\mathcal{T}_{2},\mathcal{A}\models q^{\prime}(\mathbf{a})$ and
$\mathcal{T}_{1},\mathcal{A}\not\models q^{\prime}(\mathbf{a})$.

_For ( c)_, let
$q(\mathbf{x})=\exists\mathbf{y}\,(r(x_{1},x_{2})\land\varphi(\mathbf{x}^{\prime},\mathbf{y}))$
with $x_{1},x_{2}\in\mathbf{x}$, and let
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\models q(\mathbf{a})$ be witnessed
by the match $\pi$ with $\pi(x_{i})=a_{i}$, $i=1,2$. Construct the CQ
$q(\mathbf{x}^{\prime})=\exists\mathbf{y}\,\varphi(\mathbf{x}^{\prime},\mathbf{y})$
by dropping the atom $r(x_{1},x_{2})$ (and thus possibly removing $x_{1}$
and/or $x_{2}$ from the free variables). It is clear that
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\models
q^{\prime}(\mathbf{a}^{\prime})$ for the corresponding restriction
$\mathbf{a}^{\prime}$ of the tuple $\mathbf{a}$; thus it suffices to show that
$\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}\not\models
q^{\prime}(\mathbf{a}^{\prime})$.

From $\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\models q(\mathbf{a})$ we can
conclude that $(a_{1},a_{2})\in
r^{\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}}$. By construction of
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ there is some $\mathbf{A}$-role
$r^{\prime}$ with $r^{\prime}(a_{1},a_{2})\in\mathcal{A}$ and
$\mathcal{T}_{2}\models r^{\prime}\sqsubseteq r$ (which includes the
possibility $r^{\prime}=r$, i.e., $r(a_{1},a_{2})\in\mathcal{A}$). Due to
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\text{RI}}\mathcal{T}_{2}$,
we also have $\mathcal{T}_{1}\models r^{\prime}\sqsubseteq r$ and hence
$(a_{1},a_{2})\in r^{\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}}$. This implies
the desired $\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}\not\models
q^{\prime}(\mathbf{a}^{\prime})$ because, otherwise, any match $\pi$ of
$q^{\prime}$ in $\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$ with
$\pi(x_{i})=a_{i}$, $i=1,2$, could be extended to a match of $q$.

_For ( d)_, observe that $\mathcal{T}_{2},\mathcal{A}\models q(\mathbf{a})$
and $\mathcal{T}_{1},\mathcal{A}\not\models q(\mathbf{a})$ implies
$\mathcal{T}_{2},\mathcal{A}\models q^{\prime}(\mathbf{a})$ and
$\mathcal{T}_{1},\mathcal{A}\not\models q^{\prime}(\mathbf{a})$ for some
connected component $q^{\prime}$ of $q$.

Thus, as long as $q$ violates any of the above properties, we apply the
corresponding modification; it is routine to verify that after finitely many
steps $q$ satisfies properties (a) to (d). We verify that then $q$ is weakly
tree-shaped and has at most one answer variable.

To show the latter, assume that $\mathbf{x}$ contains more than one answer
variable, say $x\neq x^{\prime}$. By (d), $q$ is connected, and thus, there is
a path from $x$ to $x^{\prime}$ in $q$, that is, a sequence of atoms
$r_{1}(z_{1},z_{2}),r_{2}(z_{2},z_{3}),\dots,r_{n}(z_{n},z_{n+1})$ with
$z_{1}=x,z_{n+1}=x^{\prime}$ and with roles $r_{i}$ such that $z_{i+1}\neq
z_{i-1}$ for every $1<i\leq n$. Let $\pi$ be a match of $q$ in
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ with $\pi(\mathbf{x})=\mathbf{a}$
and consider $z_{2}$. Because of property (c), $z_{2}$ cannot be an answer
variable. By property (a), $\pi(z_{2})$ is a successor of $\pi(z_{1})$ in
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|_{\pi(z_{1})}$. Since $\pi$ is a
match with $\pi(x^{\prime})\in\mathsf{ind}(\mathcal{A})$ and since
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|_{\pi(z_{1})}$ is weakly tree-
shaped, there has to be another element $z_{\ell}\neq z_{2}$ such that
$\pi(z_{\ell})=\pi(z_{2})$, in contradiction with property (b).

For the former, assume that $q$ is not weakly tree-shaped, that is, it
contains a cycle
$r_{1}(z_{1},z_{2}),r_{2}(z_{2},z_{3}),\dots,r_{n}(z_{n},z_{n+1})$ such that
$z_{1}=z_{n+1}$, $z_{2}\neq z_{n}$, and $z_{i+1}\neq z_{i-1}$ for every
$1<i\leq n$. Let $\pi$ be a match of $q(\mathbf{x})$ in
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ with $\pi(\mathbf{x})=\mathbf{a}$.
Since $q$ has at most one answer variable and satisfies properties (a) and
(d), there is some ABox individual $a\in\mathsf{ind}(\mathcal{A})$ such that
$\pi$ maps all variables $z_{1},\ldots,z_{n+1}$ into
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|_{a}$, which is weakly tree-shaped
by definition. Since $\pi$ is a match for the cycle in this part, there have
to be $i\neq j$ such that $z_{i},z_{j}$ are quantified variables with
$z_{i}\neq z_{j}$ and $\pi(z_{i})=\pi(z_{j})$, in contradiction to property
(b).

It remains to transform $\mathcal{A}$ into a tree-shaped ABox. Due to
properties (a) and (d), we can fix an ABox individual $a$ such that there is a
match $\pi$ of $q$ in $\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|_{a}$. Note
that, if $q$ has a single answer variable $x$, then $\pi(x)=a$. Consider the
unraveling $U_{\mathcal{A}}^{a}$ of $\mathcal{A}$ at $a$. Due to Lemma 12 (a),
$U_{\mathcal{A}}^{a}$ is still consistent with both $\mathcal{T}_{i}$. Lemma
12 (c) and the fact that the range of $\pi$ is contained in the domain of
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|_{a}$ imply
$\mathcal{T}_{2},U_{\mathcal{A}}^{a}\models q(a)$. Moreover, Lemma 12 (b) and
$\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}\not\models q(a)$ imply
$\mathcal{T}_{1},U_{\mathcal{A}}^{a}\not\models q(a)$. By compactness, there
is a finite subset $\mathcal{B}\subseteq U_{\mathcal{A}}^{a}$ with
$\mathcal{T}_{2},\mathcal{B}\models q(a)$ and
$\mathcal{T}_{1},\mathcal{B}\not\models q(a)$. Clearly, we can also assume
that $\mathcal{B}$ is connected.  ❏

We also observe an analogous result for 1tCQ entailment.

###### Proposition 14

Let $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ be $\text{Horn-}{\cal{\cal
ALCHIF}}$ TBoxes with
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\textup{RI}}\mathcal{T}_{2}$.
If
$\mathcal{T}_{1}\not\models_{\mathbf{A},\mathbf{Q}}^{\textup{1tCQ}}\mathcal{T}_{2}$,
then there is a witness $(\mathcal{A},q,a)$ where $\mathcal{A}$ is tree-shaped
and $q$ is a 1tCQ.

Proof.  Let $(\mathcal{A},a,q)$ be a witness for
$\mathcal{T}_{1}\not\not\models_{\mathbf{A},\mathbf{Q}}^{\textup{1tCQ}}\mathcal{T}_{2}$,
that is, $\mathcal{T}_{2},\mathcal{A}\models q(a)$ and
$\mathcal{T}_{1},\mathcal{A}\not\models q(a)$. As $q$ is already a 1tCQ, it
suffices to modify the ABox. Consider the unraveling $U_{\mathcal{A}}^{a}$ of
$\mathcal{A}$ at $a$. We can argue as in the proof of Proposition 13 that
there is a tree-shaped (and finite) ABox $\mathcal{B}\subseteq
U_{\mathcal{A}}^{a}$ such that $\mathcal{T}_{2},\mathcal{B}\models q(a)$ and
$\mathcal{T}_{1},\mathcal{B}\not\models q(a)$.  ❏

###  3.2 Characterization for CQ Entailment

We now develop the announced characterization of CQ entailment. Known
characterizations of entailment in Horn DLs without inverse roles (?, ?)
suggest that a first natural candidate characterization would be:
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\text{CQ}}\mathcal{T}_{2}$
iff
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\rightarrow_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$
for all tree-shaped $\mathbf{A}$-ABoxes $\mathcal{A}$ that are consistent with
$\mathcal{T}_{1}$ and $\mathcal{T}_{2}$. However, such a characterization
fails in the presence of inverse roles, in fact already for ${\cal
E\\!\\!\>LI}$.

###### Example 15

Let $\mathcal{T}_{1}=\\{A\sqsubseteq\exists s.B,~{}B\sqsubseteq\exists
r^{-}.B\\}$, $\mathcal{T}_{2}=\\{A\sqsubseteq\exists
s.B,~{}B\sqsubseteq\exists r.B\\}$, $\mathbf{A}=\\{A\\}$, and
$\mathbf{Q}=\\{r\\}$. Then both $\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$
and $\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ contain an infinite $r$-path;
the $r$-path in $\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$ has a final
element while the one in $\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ does not.
Hence, we have
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\not\rightarrow_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$.
However, it can be verified that
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\textup{CQ}}\mathcal{T}_{2}$,
see Theorem 18 below.

It is easy to turn the above candidate characterization into a correct one by
replacing homomorphisms with bounded homomorphisms, cf. Points 1 and 2 of
Lemma 10. Since we are interested in _all_ CQs over signature $\mathbf{Q}$,
however, we have to replace unbounded homomorphisms with $n$-bounded
homomorphisms, for _any_ bound $n$. In fact, the following characterization
follows from the definition of CQ entailment, Proposition 13, and Lemma 10.

###### Lemma 16

Let $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ be $\text{Horn-}{\cal{\cal
ALCHIF}}$ TBoxes with
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\textup{RI}}\mathcal{T}_{2}$.
Then
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\textup{CQ}}\mathcal{T}_{2}$
iff for all tree-shaped $\mathbf{A}$-ABoxes $\mathcal{A}$ consistent with
$\mathcal{T}_{1}$ and $\mathcal{T}_{2}$, we have
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\rightarrow^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$.

Proof.  We prove both implications via contraposition.

“$\Leftarrow$”. Assume
$\mathcal{T}_{1}\not\models_{\mathbf{A},\mathbf{Q}}^{\textup{CQ}}\mathcal{T}_{2}$
and consider a witness $(\mathcal{A},q,\mathbf{a})$. By Proposition 13, we can
assume that $\mathcal{A}$ is tree-shaped. From Lemma 11 (3), we get
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\models q(\mathbf{a})$ and
$\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}\not\models q(\mathbf{a})$. Let
$\pi$ be a match for $q(\mathbf{x})$ in
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ with
$\pi(\mathbf{x})=(\mathbf{a})$, and let $\mathcal{I}$ be the finite
subinterpretation of $\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ whose domain
$\Delta^{\mathcal{I}}$ is the range of $\pi$. We have
$\mathcal{I}\not\rightarrow_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$
because of $\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}\not\models
q(\mathbf{a})$ and $\mathcal{I}\models q(\mathbf{a})$. Hence
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\not\rightarrow^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$.

“$\Rightarrow$”. Assume
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\not\rightarrow^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$,
that is, there is a finite subinterpretation $\mathcal{I}$ of
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ with
$\mathcal{I}\not\rightarrow_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$.
We associate a query $q_{\mathcal{I}}$ with $\mathcal{I}$ as follows. The
variables in $q_{\mathcal{I}}$ take the shape $x_{a}$ with
$a\in\Delta^{\mathcal{I}}$, and $q_{\mathcal{I}}$ contains atoms $A(x_{a})$
for all $a\in A^{\mathcal{I}}$ and $r(x_{a},x_{b})$ for all $(a,b)\in
r^{\mathcal{I}}$. Answer variables of $q_{\mathcal{I}}$ are all $x_{a}$ with
$a\in\mathbf{a}$, the remaining variables are quantified. Then it can be
verified that $\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\models
q_{\mathcal{I}}(\mathbf{a})$ and
$\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}\not\models
q_{\mathcal{I}}(\mathbf{a})$.  ❏

We now show that it is possible to refine Lemma 16 so that it makes a much
more careful statement in which bounded homomorphisms and unbounded ones are
mixed. It is then possible to check the unbounded homomorphism part of the
characterization using tree automata as desired, and to deal with bounded
homomorphisms using a mosaic technique that “precompiles” relevant information
to be used in the automaton construction.

We begin with a useful lemma which shows that, under certain additional
conditions, we can extract an unbounded homomorphism from a suitable family of
bounded ones. Let $\mathcal{I}$ be an interpretation. For a signature
$\mathbf{S}$, we say that the interpretation $\mathcal{I}$ is _$\mathbf{S}$
-connected_ if between any two domain elements there is a path using only
$\mathbf{S}$-role edges, and _finitely branching_ if every domain element has
only finitely many directly connected elements.

###### Lemma 17

Let $\mathcal{I}_{1},\mathcal{I}_{2}$ be finitely branching interpretations
and let $\mathcal{I}_{1}$ be $\mathbf{S}$-connected, for a signature
$\mathbf{S}$. If there are $d_{0}\in\Delta^{\mathcal{I}_{1}}$ and
$e_{0}\in\Delta^{\mathcal{I}_{2}}$ such that for each $i\geq 0$ there is an
$\mathbf{S}$-homomorphism $h_{i}$ from $\mathcal{I}_{1}|^{d_{0}}_{i}$ to
$\mathcal{I}_{2}$ with $h_{i}(d_{0})=e_{0}$, then
$\mathcal{I}_{1}\rightarrow_{\mathbf{S}}\mathcal{I}_{2}$.

Proof.  We are going to construct an $\mathbf{S}$-homomorphism $h$ from
$\mathcal{I}_{1}$ to $\mathcal{I}_{2}$ step by step, obtaining the desired
homomorphism in the limit. We will take care that, at all times, the domain of
$h$ is finite and

  * ($*$)

there is a sequence $h_{0},h_{1},\dots$ with $h_{i}$ an
$\mathbf{S}$-homomorphism from $\mathcal{I}_{1}|^{d_{0}}_{i}$ to
$\mathcal{I}_{2}$ such that whenever $h(d)$ is already defined, then
$h_{i}(d)=h(d)$ for all $i\geq 0$.

Start with setting $h(d_{0})=e_{0}$. The original sequence
$h_{0},h_{1},\ldots$ from the lemma witnesses ($*$). Now consider the set
$\Lambda$ that consists of all elements $d\in\Delta^{\mathcal{I}_{1}}$ such
that $h(d)$ is undefined and there is an $e\in\Delta^{\mathcal{I}_{1}}$ with
$h(e)$ defined and $(e,d)\in r^{\mathcal{I}_{1}}$, for some $\mathbf{S}$-role
$r$. Since the domain of $h$ is finite and $\mathcal{I}_{1}$ is finitely
branching, $\Lambda$ is finite. By ($*$) and since $\mathcal{I}_{2}$ is
finitely branching, for each $d\in\Lambda$, there are only finitely many
$e^{\prime}$ such that $h_{i}(d)=e^{\prime}$ for some $i$. Thus, there must be
a function $\delta:\Lambda\rightarrow\Delta^{\mathcal{I}_{2}}$ such that, for
infinitely many $i$, we have $h_{i}(d)=\delta(d)$, for all $d\in\Lambda$.
Extend $h$ accordingly, that is, set $h(d)=\delta(d)$ for all $d\in\Lambda$.
Clearly, the sequence $h_{0},h_{1},\dots$ from ($*$) before the extension is
no longer sufficient to witness ($*$) after the extension. We fix this by
skipping homomorphisms that do not respect $\delta$, that is, define a new
sequence $h^{\prime}_{0},h^{\prime}_{1},\dots$ by using as $h^{\prime}_{i}$
the restriction of $h_{j}$ to the domain of $\mathcal{I}_{1}|^{d_{0}}_{i}$
where $j\geq i$ is smallest such that $h_{j}(d)=\delta(d)$ for all
$d\in\Lambda$. This finishes the construction. The lemma follows from the fact
that, due to $\mathbf{S}$-connectedness of $\mathcal{I}_{1}$, every element is
eventually reached. Note that we automatically have $h(a)=a$ for all
individual names $a$ (as required), no matter whether $d_{0}$ is an individual
name or not.  ❏

We continue with introducing notation relevant for the refinement of Lemma 16.
For a signature $\mathbf{S}$, we use
$\mathcal{I}|^{\mathsf{con}}_{\mathbf{S}}$ to denote the restriction of the
interpretation $\mathcal{I}$ to those elements that can be reached from an
ABox individual by traveling along $\mathbf{S}$-roles (forwards or backwards).
An _$\mathbf{S}$ -subtree in_ $\mathcal{I}_{\mathcal{T},\mathcal{A}}$ is a
maximal weakly tree-shaped, $\mathbf{S}$-connected sub-interpretation
$\mathcal{I}$ of $\mathcal{I}_{\mathcal{T},\mathcal{A}}$ that does not
comprise any ABox individuals. The _root_ of $\mathcal{I}$ is the (unique)
element of $\Delta^{\mathcal{I}}$ that can be reached from an ABox individual
on a shortest path among all elements of $\Delta^{\mathcal{I}}$.

###### Theorem 18

Let $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ be $\text{Horn-}{\cal{\cal
ALCHIF}}$ TBoxes with
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\textup{RI}}\mathcal{T}_{2}$.
Then
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\textup{CQ}}\mathcal{T}_{2}$
iff for all tree-shaped $\mathbf{A}$-ABoxes $\mathcal{A}$ consistent with
$\mathcal{T}_{1}$ and $\mathcal{T}_{2}$, and for all weakly tree-shaped and
finitely branching models $\mathcal{I}_{1}$ of $\mathcal{A}$ and
$\mathcal{T}_{1}$, the following hold:

  1. (1)

$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|^{\mathsf{con}}_{\mathbf{Q}}\rightarrow_{\mathbf{Q}}\mathcal{I}_{1}$;

  2. (2)

for all $\mathbf{Q}$-subtrees $\mathcal{I}$ in
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$, one of the following holds:

    1. (a)

$\mathcal{I}\rightarrow_{\mathbf{Q}}\mathcal{I}_{1}$;

    2. (b)

$\mathcal{I}\rightarrow^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathsf{tp}_{\mathcal{I}_{1}}(a)}$
for some $a\in\mathsf{ind}(\mathcal{A})$.

Proof.  “$\Leftarrow$”. Suppose that
$\mathcal{T}_{1}\not\models_{\mathbf{A},\mathbf{Q}}^{\text{CQ}}\mathcal{T}_{2}$.
By Proposition 13, there is a tree-shaped $\mathbf{A}$-ABox $\mathcal{A}$
consistent with both $\mathcal{T}_{i}$, and a weakly tree-shaped
$\mathbf{Q}$-CQ $q$ such that either

  1. (1′)

$q$ has a single answer variable and there is an element
$a\in\mathsf{ind}(\mathcal{A})$ such that $\mathcal{T}_{2},\mathcal{A}\models
q(a)$ but $\mathcal{T}_{1},\mathcal{A}\not\models q(a)$, or

  2. (2′)

$q$ is Boolean and $\mathcal{T}_{2},\mathcal{A}\models q$ but
$\mathcal{T}_{1},\mathcal{A}\not\models q$.

In case (1′), let $\pi$ be a match of $q$ in
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ with $\pi(x)=a$. Since $q$
contains an answer variable, we must have
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|^{\mathsf{con}}_{\mathbf{Q}}\not\rightarrow_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$
as otherwise the composition of $\pi$ and the witnessing homomorphism shows
$\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}\models q(a)$, which is not the
case. Thus, Condition (1) is violated for
$\mathcal{I}_{1}=\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$.

In case (2′), consider a match $\pi$ of $q$ in
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$, and let $\mathcal{I}$ be the
restriction of $\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ to the elements in
the range of $\pi$. Clearly, we have
$\mathcal{I}\not\rightarrow_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$.
Consequently, we also have
$\mathcal{I}\not\rightarrow^{n}_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$
where $n$ is the number of variables in $q$, implying that Conditions (2a) and
(2b) are both false.

“$\Rightarrow$”. Assume that
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\text{CQ}}\mathcal{T}_{2}$
and let $\mathcal{A}$ be a tree-shaped $\mathbf{A}$-ABox consistent with both
$\mathcal{T}_{i}$. Moreover, let $\mathcal{I}_{1}$ be a weakly tree-shaped,
finitely branching model of $\mathcal{A}$ and $\mathcal{T}_{1}$.

For Condition (1), and let
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|^{\mathsf{con}}_{\mathbf{Q}}$ be
the disjoint union of the connected interpretations
$\mathcal{J}_{1},\dots,\mathcal{J}_{k}$. In each $\mathcal{J}_{i}$, we find at
least one individual $a_{i}$ from $\mathsf{ind}(\mathcal{A})$. Let
$\ell\in\\{1,\dots,k\\}$. By
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\text{CQ}}\mathcal{T}_{2}$
and Lemma 16, we have
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\to^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$
and hence, by Lemma 11 (2),
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\to^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{1}$.
By Lemma 10 (3), we find a sequence $h_{0},h_{1},\dots$ such that $h_{i}$ is a
$\mathbf{Q}$-homomorphism from $\mathcal{J}_{\ell}|^{a_{\ell}}_{i}$ to
$\mathcal{I}_{1}$. Note that we must have $h_{i}(a_{\ell})=a_{\ell}$ for all
$i$. Thus, Lemma 17 yields
$\mathcal{J}_{\ell}\rightarrow_{\mathbf{Q}}\mathcal{I}_{1}$ and, in summary,
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|^{\mathsf{con}}_{\mathbf{Q}}\rightarrow_{\mathbf{Q}}\mathcal{I}_{1}$.

For Condition (2), let $\mathcal{I}$ be a $\mathbf{Q}$-subtree in
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ with root $d_{0}$. By Lemma 16, we
have
$\mathcal{I}\to^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$.
By Lemma 10 (3), there is a sequence $h_{0},h_{1},\dots$ such that $h_{i}$ is
a $\mathbf{Q}$-homomorphism from $\mathcal{I}|^{d_{0}}_{i}$ to
$\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$. We distinguish two cases, leading
to (2)(a) and (2)(b), respectively.

First assume that there is an
$e_{0}\in\Delta^{\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}}$ such that
$h_{i}(d_{0})=e_{0}$ for infinitely many $i$. Construct a new sequence
$h^{\prime}_{0},h^{\prime}_{1},\dots$ with $h^{\prime}_{i}$ a
$\mathbf{Q}$-homomorphism from $\mathcal{I}|^{d_{0}}_{i}$ to
$\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$ by skipping homomorphisms that do
not map $d_{0}$ to $e_{0}$, that is, $h^{\prime}_{i}$ is the restriction of
$h_{j}$ to the domain of $\mathcal{I}|^{d_{0}}_{i}$ where $j\geq i$ is
smallest such that $h_{j}(d_{0})=e_{0}$. Clearly,
$h^{\prime}_{i}(d_{0})=e_{0}$ for all $i$. Thus, Lemma 17 yields
$\mathcal{I}\rightarrow_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$
and thus, by Lemma 11 (2)
$\mathcal{I}\rightarrow_{\mathbf{Q}}\mathcal{I}_{1}$.

Otherwise, there is no
$e_{0}\in\Delta^{\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}}$ such that
$h_{i}(d_{0})=e_{0}$ for infinitely many $i$. We can assume that there is an
$a_{0}\in\mathsf{ind}(\mathcal{A})$ such that
$h_{i}(d_{0})\in\Delta^{\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}|_{a_{0}}}$
for all $i$; in fact, there must be an $a_{0}$ such that
$h_{i}(d_{0})\in\Delta^{\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}|_{a_{0}}}$
for infinitely many $i$ and we can again skip homomorphisms to achieve this
for all $i$. It is important to note that the remaining homomorphisms do not
necessarily all map domain elements of $\mathcal{I}$ to elements in
$\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}|_{a_{0}}$ due to the presence of
inverse roles. Now, since $\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}$ is
finitely branching, for all $i,n\geq 0$ we must find a $j\geq i$ such that
$h_{j}(d_{0})$ is a domain element whose distance from $a_{0}$ exceeds $n$
(otherwise the previous case would apply). Based on this observation, we
construct a sequence of homomorphisms $h^{\prime}_{0},h^{\prime}_{1},\dots$ as
follows. For all $i\geq 0$, let $h^{\prime}_{i}$ be the restriction of some
$h^{\prime}_{j}$ to the domain of $\mathcal{I}|^{d_{0}}_{i}$ where $j\geq i$
is smallest such that the distance of $h_{j}(d_{0})$ from $a_{0}$ exceeds $i$.
It should be clear that each $h_{i}^{\prime}$ is a $\mathbf{Q}$-homomorphism
from $\mathcal{I}|^{d_{0}}_{i}$ to
$\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}|_{a_{0}}$, hence
$\mathcal{I}\rightarrow^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}|_{a_{0}}$,
by Lemma 10 (3).

Now Lemma 11 (2) and Condition (1) of homomorphisms imply
$\mathsf{tp}_{\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}}(a_{0})\subseteq\mathsf{tp}_{\mathcal{I}_{1}}(a_{0})$;
thus by Lemma 11 (4) we have
$\mathcal{I}_{\mathcal{T}_{1},\mathcal{A}}|_{a_{0}}\rightarrow\mathcal{I}_{\mathcal{T}_{1},\mathsf{tp}_{\mathcal{I}_{1}}(a_{0})}$.
Altogether we get
$\mathcal{I}\rightarrow^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},\mathsf{tp}_{\mathcal{I}_{1}}(a_{0})}$
as required.  ❏

###  3.3 Characterization for 1tCQ Entailment

We now give a 1tCQ version of Theorem 18, that is, a characterization of 1tCQ-
entailment. We use (unbounded) simulations in place of homomorphisms.

###### Theorem 19

Let $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ be $\text{Horn-}{\cal{\cal
ALCHIF}}$ TBoxes with
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\textup{RI}}\mathcal{T}_{2}$.
Then the following three conditions are equivalent:

  1. (a)

$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\textup{1tCQ}}\mathcal{T}_{2}$;

  2. (b)

$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\preceq_{\mathbf{Q}}\mathcal{I}_{1}$
for all tree-shaped $\mathbf{A}$-ABoxes $\mathcal{A}$ that are consistent with
$\mathcal{T}_{1}$ and $\mathcal{T}_{2}$, and for all weakly tree-shaped,
finitely branching models $\mathcal{I}_{1}$ of $\mathcal{A}$ and
$\mathcal{T}_{1}$.

Proof.

(b) $\Rightarrow$ (a). This implication is analogous to the “$\Rightarrow$”
direction in the proof of Theorem 18, but using Proposition 14 in place of
Proposition 13. This rules out Case (2′) and thus Condition (2) from Theorem
18. In Condition (1), we can replace homomorphisms with simulations since the
witnessing CQ is a 1tCQ.

(a) $\Rightarrow$ (b). For the proof of this direction, we need a bounded
variant of simulations, analogously to bounded homomorphisms. We write
$\mathcal{I}_{1}\preceq^{n}_{\mathbf{Q}}\mathcal{I}_{2}$ if for any
subinterpretation $\mathcal{I}^{\prime}_{1}$ of $\mathcal{I}_{1}$ with
$|\Delta^{\mathcal{I}^{\prime}_{1}}|\leq n$, we have
$\mathcal{I}^{\prime}_{1}\preceq_{\mathbf{Q}}\mathcal{I}_{2}$. Moreover, we
write $\mathcal{I}_{1}\preceq^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{2}$ if
$\mathcal{I}_{1}\preceq^{n}_{\mathbf{Q}}\mathcal{I}_{2}$, for any $n$.

Assume that
$\mathcal{T}_{1}\models_{\mathbf{A},\mathbf{Q}}^{\text{1tCQ}}\mathcal{T}_{2}$
and let $\mathcal{A}$ be a tree-shaped $\mathbf{Q}$-ABox that is consistent
with both $\mathcal{T}_{i}$. Let $\mathcal{I}_{1}$ be a weakly tree-shaped,
finitely branching model of $\mathcal{T}_{1}$ and $\mathcal{A}$. We first show
the following.
Claim.
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|_{a}\preceq^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{1}$
for all $a\in\mathsf{ind}(\mathcal{A})$.
Assume to the contrary that
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|_{a}\npreceq^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{1}$.
Then
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|_{a}\npreceq^{n}_{\mathbf{Q}}\mathcal{I}_{1}$
for some $n$, that is, there is a subinterpretation $\mathcal{I}$ of
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|_{a}$ with
$|\Delta^{\mathcal{I}}|\leq n$ such that
$\mathcal{I}\npreceq_{\mathbf{Q}}\mathcal{I}_{1}$. We can assume w.l.o.g. that
$\mathcal{I}$ is connected and contains $a$ (otherwise we just extend
$\mathcal{I}$ and increase $n$ accordingly). Let $q_{\mathcal{I}}$ be
$\mathcal{I}$ viewed as a weakly tree-shaped CQ with domain elements viewed as
variables and $a$ viewed as the only answer variable. Clearly,
$\mathcal{I}\models q(a)$ and thus
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|_{a}\models q(a)$. Let $\pi$ be a
witnessing match of $q$ in $\mathcal{I}$. To transform $q$ into a 1tCQ,
perform the following operations:

  * •

remove all atoms of the form $r(a,a)$;

  * •

Split multi-edges in $q$ by duplicating subtree queries: if
$r_{1}(z,z^{\prime}),\dots,r_{n}(z,z^{\prime})$ are in $q$ where
$r_{1},\dots,r_{n}$ are potentially inverse roles and $z^{\prime}$ is a
successor of $z$ when the answer variable is viewed as the root of $q$, then
introduce $n$ copies of the subtree rooted at $z^{\prime}$ and connect $z$ to
each copy with one of the roles $r_{1},\dots,r_{n}$. Remove the subtree rooted
at $z^{\prime}$.

The result of this transformation is a 1tCQ $q^{\prime}$, which still
satisfies $\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}\models q^{\prime}(a)$. On
the other hand, $\mathcal{I}_{1}\not\models q^{\prime}(a)$ because, otherwise,
a match $\pi^{\prime}$ of $q^{\prime}(x)$ in $\mathcal{I}_{1}$ would give rise
to a simulation of $\mathcal{I}$ in $\mathcal{I}_{1}$. This finishes the proof
of the claim.

The claim implies that for all $a\in\mathsf{ind}(\mathcal{A})$ and all $i\geq
0$, there is a $\mathbf{Q}$-simulation from
$(\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|_{a})|^{a}_{i}$ to
$\mathcal{I}_{1}$: for every $a$, the situation parallels Condition (3a) of
Lemma 10 with homomorphisms replaced by simulations. We can use exactly the
same arguments as in the proof of Lemma 10 (3) to show that there is a
$\mathbf{Q}$-simulation from
$(\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}|_{a})|^{a}_{i}$ to
$\mathcal{I}_{1}$. The union of these simulations, for all
$a\in\mathsf{ind}(\mathcal{A})$, is the desired $\mathbf{Q}$-simulation from
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ to $\mathcal{I}_{1}$.  ❏

##  4 Decidability and Complexity

Our aim is to prove the following result.

###### Theorem 20

In $\text{Horn-}{\cal{\cal ALCHIF}}$ and any of its fragments that contains
${\cal E\\!\\!\>LI}$ or Horn-${\cal ALC}$, the following problems are
2ExpTime-complete: $(\mathbf{A},\mathbf{Q})$-CQ entailment,
$(\mathbf{A},\mathbf{Q})$-CQ inseparability, and $(\mathbf{A},\mathbf{Q})$-CQ
conservative extensions. This holds even when $\mathbf{A}=\mathbf{Q}$.
Moreover, these problems can be solved in time
$2^{2^{p(|\mathcal{T}_{2}|\mathsf{log}|\mathcal{T}_{1}|)}}$, where $p$ is a
polynomial.

The lower bounds have been established by ? (?). To obtain the upper bounds,
we use an approach based on the characterization provided by Theorem 18 that
combines a mosaic technique with tree automata. More precisely, we first
observe that Condition (2b) is the only part of Theorem 18 concerned with
bounded homomorphisms, and that addressing this condition requires us to check
for a given $\mathbf{Q}$-subtree $\mathcal{I}$ in
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}}$ and a $\mathcal{T}_{1}$-type
$t_{1}$, whether
$\mathcal{I}\rightarrow^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},t_{1}}$.
In fact, it suffices to consider subtrees $\mathcal{I}$ whose root is
connected only by non-$\mathbf{Q}$ roles as all $\mathcal{I}$ that do not
satisfy this condition are not maximal or treated by Condition (1) of Theorem
18. An analysis of universal models reveals that such $\mathcal{I}$ are
completely determined by the $\mathcal{T}_{2}$-type $t_{2}$ of their root and
are in fact identical to
$\mathcal{I}_{\mathcal{T}_{2},t_{2}}|^{\mathsf{con}}_{\mathbf{Q}}$.444This
depends on the assumption that the root is connected only by non-$\mathbf{Q}$
roles, c.f. Condition (ii) from the definition of universal models.  This
gives rise to the problem of deciding whether
$\mathcal{I}_{\mathcal{T}_{2},t_{2}}|^{\mathsf{con}}_{\mathbf{Q}}\rightarrow^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},t_{1}}$,
for given $\mathcal{T}_{1},\mathcal{T}_{2},t_{1},t_{2}$, and $\mathbf{Q}$. We
show that this problem can be solved in 2ExpTime using a mosaic technique and
then use that result as a black box in an automata based approach to prove the
upper bound.

###  4.1 Mosaics

The aim of this section is to prove the following.

###### Theorem 21

Given two Horn-${\cal ALCHIF}$ TBoxes $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$,
a $\mathcal{T}_{1}$-type $t_{1}$, a $\mathcal{T}_{2}$-type $t_{2}$, and a
signature $\mathbf{S}$, it can be decided in time
$2^{2^{p(|\mathcal{T}_{2}|\mathsf{log}|\mathcal{T}_{1}|)}}$ whether
$\mathcal{I}_{\mathcal{T}_{2},t_{2}}|^{\mathsf{con}}_{\mathbf{S}}\rightarrow^{\mathsf{fin}}_{\mathbf{S}}\mathcal{I}_{\mathcal{T}_{1},t_{1}}$,
where $p$ is a polynomial.

We prove Theorem 21 by replacing bounded homomorphisms with unbounded ones
and, to compensate for this, further replacing the target interpretation
$\mathcal{I}_{\mathcal{T}_{1},t_{1}}$ with a suitably constructed class of
interpretations.

To illustrate, consider Example 15 and let $t_{1}=t_{2}=\\{B\\}$. The
difference between
$\mathcal{I}_{\mathcal{T}_{2},t_{2}}\rightarrow^{\mathsf{fin}}_{\mathbf{S}}\mathcal{I}_{\mathcal{T}_{1},t_{1}}$
and
$\mathcal{I}_{\mathcal{T}_{2},t_{2}}\rightarrow_{\mathbf{S}}\mathcal{I}_{\mathcal{T}_{1},t_{1}}$
is that unbounded homomorphisms fail once they “reach the root” of
$\mathcal{I}_{\mathcal{T}_{1},t_{1}}$ while bounded homomorphisms can,
depending on the bound, map the root of $\mathcal{I}_{\mathcal{T}_{2},t_{2}}$
deeper and deeper into $\mathcal{I}_{\mathcal{T}_{1},t_{1}}$, thus never
reaching its root. The latter is possible because
$\mathcal{I}_{\mathcal{T}_{1},t_{1}}$ is regular in the sense that any two
elements which have the same type are the root of isomorphic subtree
interpretations. This is of course not only true in this example, but in any
universal model. To transition back from bounded to unbounded homomorphisms,
we replace $\mathcal{I}_{\mathcal{T}_{1},t_{1}}$ with a class of
interpretations that can be seen as a “backwards regularization” of
$\mathcal{I}_{\mathcal{T}_{1},t_{1}}$. In our concrete example,
$\mathcal{I}_{\mathcal{T}_{1},t_{1}}$ contains an element that has the same
type as the root of $\mathcal{I}_{\mathcal{T}_{1},t_{1}}$ and that has a
predecessor $d$. This would lead us to consider (among others) the
interpretation obtained from $\mathcal{I}_{\mathcal{T}_{1},t_{1}}$ by adding a
predecessor of the same type as $d$ and possibly adding further predecessors,
even ad infinitum. We now make this idea precise.

A _rooted weakly tree-shaped interpretation_ is a pair $(\mathcal{I},d_{0})$
with $\mathcal{I}$ a weakly tree-shaped interpretation and
$d_{0}\in\Delta^{\mathcal{I}}$ a _root_. The root imposes a direction on
$\mathcal{I}$ and thus allows us to speak about successors and predecessors,
that is, when $(d,e)\in r^{\mathcal{I}}$, then $e$ is a _successor_ of $d$ if
the distance of $e$ to $d_{0}$ in the undirected graph
$(\Delta^{\mathcal{I}},\\{\\{d,e\\}\mid(d,e)\in r^{\mathcal{I}}\text{ for some
}r\in{\sf N_{C}}\\})$ is larger than the distance of $d$ to $d_{0}$, and a
_predecessor_ otherwise. Note that the direction does not correspond to the
distinction between roles and inverse roles, but rather reflects the
directedness of universal models $\mathcal{I}_{\mathcal{T},t}$, which can be
viewed as being rooted weakly tree-shaped:
$\Delta^{\mathcal{I}_{\mathcal{T},t}}$ is a set of paths and the root of
$\mathcal{I}_{\mathcal{T},t}$ is the unique path in
$\Delta^{\mathcal{I}_{\mathcal{T},t}}$ of minimum length.

Throughout the section, we work with sets $\rho$ of (possibly inverse) roles;
in particular, we say that $b$ is a _$\rho$ -successor_ of $a$ if
$\rho=\\{r\mid(a,b)\in r^{\mathcal{I}}\\}$. Let $\mathcal{T}$ be a
$\text{Horn-}{\cal{\cal ALCHIF}}$ TBox and let $\mathsf{tp}(\mathcal{T})$ be
the set of all $\mathcal{T}$-types consistent with $\mathcal{T}$. For every
$t_{0}\in\mathsf{tp}(\mathcal{T})$, we use $\mathsf{tp}(\mathcal{T},t_{0})$ to
denote the set of all $t\in\mathsf{tp}(\mathcal{T})$ that occur in the
universal model $\mathcal{I}_{\mathcal{T},t_{0}}$ of $t_{0}$ and
$\mathcal{T}$. Furthermore, given a rooted weakly tree-shaped interpretation
$(\mathcal{I},d_{0})$ and an element $d\in\Delta^{\mathcal{I}}$, the
_1-neighborhood of $d$ in $\mathcal{I}$_ is a tuple
$n_{1}^{\mathcal{I}}(d)=(t^{-},\rho,t,S)$ such that

  1. (a)

$t=\mathsf{tp}_{\mathcal{I}}(d)$;

  2. (b)

if $d$ is the $\rho^{\prime}$-successor of some
$d^{-}\in\Delta^{\mathcal{I}}$, then $t^{-}=\mathsf{tp}_{\mathcal{I}}(d^{-})$
and $\rho=\rho^{\prime}$, otherwise $\rho=t^{-}=\bot$;

  3. (c)

$S$ is the set of all pairs $(\rho^{\prime},t^{\prime})$ such that there is a
$\rho^{\prime}$-successor $d^{\prime}$ of $d$ with
$t^{\prime}=\mathsf{tp}_{\mathcal{I}}(d^{\prime})$.

We further write
$(t^{-}_{1},\rho_{1},t_{1},S_{1})\sqsubseteq(t^{-}_{2},\rho_{2},t_{2},S_{2})$
if $t_{1}=t_{2}$, $S_{1}\subseteq S_{2}$ and, if $\rho_{1}\neq\bot$, then
$\rho_{1}=\rho_{2}$ and $t^{-}_{1}=t^{-}_{2}$.

In the following, we define the class
$\mathsf{mod}_{\omega}(\mathcal{T},t_{0})$ of models of $\mathcal{T}$ that we
consider as homomorphism targets. Each model from this class is obtained as
the limit of a (finite or infinite) sequence of rooted weakly tree-shaped
interpretations. Start to construct the sequence by choosing a type
$t\in\mathsf{tp}(\mathcal{T},t_{0})$ and defining
$\mathcal{I}=(\\{d_{0}\\},\cdot^{\mathcal{I}})$ such that
$\mathsf{tp}_{\mathcal{I}}(d_{0})=t$. The remaining sequence is obtained by
repeatedly applying the following rule:

  1. (R)

Let $d\in\Delta^{\mathcal{I}}$. Choose some
$e\in\Delta^{\mathcal{I}_{\mathcal{T},t_{0}}}$ such that
$n_{1}^{\mathcal{I}}(d)\sqsubseteq
n_{1}^{\mathcal{I}_{\mathcal{T},t_{0}}}(e)$, and add to $d$ the predecessor
and/or successors required to achieve
$n_{1}^{\mathcal{I}}(d)=n_{1}^{\mathcal{I}_{\mathcal{T},t_{0}}}(e)$. If a new
predecessor is added, it becomes the new root.

Note that rule application does not need to be fair nor exhaustive. Now,
$\mathsf{mod}_{\omega}(\mathcal{T},t_{0})$ is the set of all (weakly tree-
shaped but not rooted) interpretations $\mathcal{I}$ that can be obtained as
the limit of a sequence constructed in the described way.

###### Lemma 22

Let $\mathcal{T}$ be a $\text{Horn-}{\cal{\cal ALCHIF}}$ TBox,
$t_{0}\in\mathsf{tp}(\mathcal{T})$, and $\mathcal{I}$ a finitely branching,
weakly tree-shaped interpretation. Then
$\mathcal{I}\rightarrow^{\mathsf{fin}}_{\mathbf{S}}\mathcal{I}_{\mathcal{T},t_{0}}$
iff there is a $\mathcal{J}\in\mathsf{mod}_{\omega}(\mathcal{T},t_{0})$ with
$\mathcal{I}\rightarrow_{\mathbf{S}}\mathcal{J}$.

Proof.  “$\Rightarrow$”. Suppose
$\mathcal{I}\rightarrow^{\mathsf{fin}}_{\mathbf{S}}\mathcal{I}_{\mathcal{T},t_{0}}$
for some finitely branching, weakly tree-shaped interpretation $\mathcal{I}$,
and choose a root $d_{0}$ of $\mathcal{I}$. By Lemma 10 (3), there is a
sequence $h_{0},h_{1},\ldots$ such that $h_{i}$ is an
$\mathbf{S}$-homomorphism from $\mathcal{I}|^{d_{0}}_{i}$ to
$\mathcal{I}_{\mathcal{T},t_{0}}$. Note that both $\mathcal{I}$ and
$\mathcal{I}_{\mathcal{T},t_{0}}$ are finitely branching. By skipping
homomorphisms (similar to the proof of Lemma 17), we can thus construct a new
sequence $h_{0}^{\prime},h_{1}^{\prime},\ldots$ such that $h_{i}^{\prime}$ is
an $\mathbf{S}$-homomorphism from $\mathcal{I}|_{i}^{d_{0}}$ to
$\mathcal{I}_{\mathcal{T},t_{0}}$ and, additionally, for every $i\geq 0$ and
every $d\in\Delta^{\mathcal{I}|^{d_{0}}_{i}}$ the following properties hold:

  1. (i)

$n_{1}^{\mathcal{I}_{\mathcal{T},t_{0}}}(h_{i}^{\prime}(d))=n_{1}^{\mathcal{I}_{\mathcal{T},t_{0}}}(h_{j}^{\prime}(d))$
for all $j$ with $j\geq i$;

  2. (ii)

if $e$ is a successor of $d$ in $\mathcal{I}$, then one of the following is
the case:

     * •

$h_{j}^{\prime}(e)$ is the predecessor of $h_{j}^{\prime}(d)$ in
$\mathcal{I}_{\mathcal{T},t_{0}}$, for all $j$ with $j\geq i$, or

     * •

$h_{j}^{\prime}(e)$ is a successor of $h_{j}^{\prime}(d)$ in
$\mathcal{I}_{\mathcal{T},t_{0}}$, and there is some $(\rho,t)$ in component
$S$ of $n_{1}^{\mathcal{I}_{\mathcal{T},t_{0}}}(h_{i}^{\prime}(d))$ such that
for all $j$ with $j\geq i$, we have
$\rho=\\{r\mid(h_{j}^{\prime}(d),h_{j}^{\prime}(e))\in
r^{\mathcal{I}_{\mathcal{T},t_{0}}}\\}$ and $h_{j}^{\prime}(e)=t$.

Guided by $h_{i}^{\prime}$, we construct a sequence of rooted weakly tree-
shaped interpretations $(\mathcal{J}_{0},e_{0}),$
$(\mathcal{J}_{1},e_{1}),\ldots$ and a sequence $g_{0},g_{1},\ldots$ with
$g_{i}$ an $\mathbf{S}$-homomorphism from $\mathcal{I}|^{d_{0}}_{i}$ to
$\mathcal{J}_{i}$ such that for every $i,j$ with $0\leq i\leq j$ and every
$d\in\Delta^{\mathcal{I}|^{d_{0}}_{i}}$, we have $g_{i}(d)=g_{j}(d)$. The
required interpretation
$\mathcal{J}\in\mathsf{mod}_{\omega}(\mathcal{T},t_{0})$ is obtained in the
limit. Throughout the construction, we maintain the invariant

$n_{1}^{\mathcal{J}_{i}}(g_{i}(d))\sqsubseteq
n_{1}^{\mathcal{I}_{\mathcal{T},t_{0}}}(h_{i}^{\prime}(d))$

for all $i,d$ such that $g_{i}(d)$ is defined.

We start with $\mathcal{J}_{0}=(\\{e_{0}\\},\cdot^{\mathcal{J}_{0}})$ such
that
$\mathsf{tp}_{\mathcal{J}_{0}}(e_{0})=\mathsf{tp}_{\mathcal{I}_{\mathcal{T},t_{0}}}(h_{0}^{\prime}(d_{0}))$,
choose $e_{0}$ as the root and set $g_{0}(d_{0})=e_{0}$. Clearly $(*)$ is
satisfied. Assuming that $(\mathcal{J}_{i},e_{i})$ and $g_{i}$ are already
defined, we extend them to $(\mathcal{J}_{i+1},e_{i+1})$ and $g_{i+1}$ as
follows. Choose some $d\in\Delta^{\mathcal{I}|^{d_{0}}_{i}}$ and
$d^{\prime}\notin\Delta^{\mathcal{I}|^{d_{0}}_{i}}$ such that
$(d,d^{\prime})\in r^{\mathcal{I}}$ for some role $r$. By invariant $(*)$ and
Point (i), we have $n_{1}^{\mathcal{J}_{i}}(g_{i}(d))\sqsubseteq
n_{1}^{\mathcal{I}_{\mathcal{T},t_{0}}}(h_{j}^{\prime}(d))$ for all $j\geq i$.
Thus, we can apply (R) to $g_{i}(d)$ in $\mathcal{J}_{i}$ and
$h^{\prime}_{i}(d)$ in $\Delta^{\mathcal{I}_{\mathcal{T},t_{0}}}$. More
precisely, we obtain $\mathcal{J}_{i+1}$ from $\mathcal{J}_{i}$ by adding a
predecessor and/or successors to achieve

$n_{1}^{\mathcal{J}_{i+1}}(g_{i}(d))=n_{1}^{\mathcal{I}_{\mathcal{T},t_{0}}}(h_{i}^{\prime}(d)).$

Moreover, $e_{i+1}$ is the root of $\mathcal{J}_{i+1}$, updated according to
(R). To define $g_{i+1}$, we extend $g_{i}$ to $d^{\prime}$ by distinguishing
two cases according to Point (ii):

  * •

Suppose $h^{\prime}_{j}(d^{\prime})$ is the predecessor of $h^{\prime}_{j}(d)$
for all $j\geq i$. We set $g_{i+1}(d^{\prime})$ to the predecessor of
$g_{i}(d)$ (exists due to ($**$)). Clearly, $(*)$ is satisfied also for
$g_{i+1}(d^{\prime})$.

  * •

Suppose $h^{\prime}_{j}(d^{\prime})$ is a successor of $h^{\prime}_{j}(d)$ for
all $j\geq i$, and let $(\rho,t)$ be as described. Let
$e\in\Delta^{\mathcal{J}_{i+1}}$ be an element with
$\mathsf{tp}_{\mathcal{J}_{i+1}}(e)=t$ and $\rho=\\{r\mid(g_{i}(d),e)\in
r^{\mathcal{J}_{i+1}}\\}$. Note that such an element exists due to ($**$). Set
$g_{i+1}(d^{\prime})=e$. Clearly, $(*)$ is satisfied also for
$g_{i+1}(d^{\prime})$.

The construction of $\mathcal{J}$ and $h$ is finished by setting
$h=\bigcup_{i\geqslant 0}g_{i}$ and $\mathcal{J}^{\prime}=\bigcup_{i\geqslant
0}\mathcal{J}_{i}$.

“$\Leftarrow$”. Suppose there is a
$\mathcal{J}\in\mathsf{mod}_{\omega}(\mathcal{T},t_{0})$ with
$\mathcal{I}\to_{\mathbf{S}}\mathcal{J}$. It suffices to show
$\mathcal{J}\to^{\mathsf{fin}}\mathcal{I}_{\mathcal{T},t_{0}}$. Let
$(\mathcal{J}_{0},d_{0}),(\mathcal{J}_{1},d_{1}),\ldots$ be the sequence of
rooted weakly tree-shaped interpretations whose limit is $\mathcal{J}$. We
verify the following claim, which implies
$\mathcal{J}\rightarrow^{\mathsf{fin}}\mathcal{I}_{\mathcal{T},t_{0}}$.

Claim. For all $i\geq 0$, we have:

  1. (i)

there is an $e_{0}\in\Delta^{\mathcal{I}_{\mathcal{T},t_{0}}}$ with
$\mathsf{tp}_{\mathcal{J}_{i}}(d_{i})=\mathsf{tp}_{\mathcal{I}_{\mathcal{T},t_{0}}}(e_{0})$;

  2. (ii)

for all $e_{0}\in\Delta^{\mathcal{I}_{\mathcal{T},t_{0}}}$ with
$\mathsf{tp}_{\mathcal{J}_{i}}(d_{i})\subseteq\mathsf{tp}_{\mathcal{I}_{\mathcal{T},t_{0}}}(e_{0})$,
we have
$(\mathcal{J}_{i},d_{i})\rightarrow(\mathcal{I}_{\mathcal{T},t_{0}},e_{0})$.

We prove the claim by induction on $i$. For $i=0$, Points (i) and (ii) follow
from the definition of $\mathcal{J}_{0}$. For the inductive step, consider
$\mathcal{J}_{i+1}$ and suppose (R) has been applied to some
$d\in\Delta^{\mathcal{J}_{i}}$ and
$e\in\Delta^{\mathcal{I}_{\mathcal{T},t_{0}}}$.

For $i>0$, observe first that Point (i) is trivially preserved when
$d_{i+1}=d_{i}$. In case $d_{i+1}$ is the predecessor of $d_{i}$, it is
preserved by the condition on the choice of $e$ in (R): $e$ has the same type
as $d_{i}$ and the predecessor $e^{\prime}$ of $e$ has the same type as
$d_{i+1}$.

For Point (ii), we distinguish two cases.

Case 1. Suppose the application of (R) has not added any predecessors to $d$.
In particular, we then have $d_{i+1}=d_{i}$. For Point (ii), take any $e_{0}$
with
$\mathsf{tp}_{\mathcal{J}_{i}}(d_{i+1})\subseteq\mathsf{tp}_{\mathcal{I}_{\mathcal{T},t_{0}}}(e_{0})$.
As $d_{i}=d_{i+1}$, induction hypothesis implies that there is a homomorphism
$h:(\mathcal{J}_{i},d_{i+1})\to(\mathcal{I}_{\mathcal{T},t_{0}},e_{0})$. We
extend $h$ to the domain of $\mathcal{J}_{i+1}$ by doing the following for
each newly added successor $d^{\prime}$ of $d$.

Let $\mathsf{tp}_{\mathcal{J}_{i+1}}(d)=t$ and
$\mathsf{tp}_{\mathcal{J}_{i+1}}(d^{\prime})=t^{\prime}$ and
$\rho=\\{r\mid(d,d^{\prime})\in r^{\mathcal{J}_{i+1}}\\}$. By the choice of
$e$ in (R), $e$ is of type $t$ and has a $\rho$-successor of type
$t^{\prime}$. By definition of the universal model, there is some $r\in\rho$
with $t\rightsquigarrow_{r}^{\mathcal{T}}t^{\prime}$ and
$\rho=\\{s\mid\mathcal{T}\models r\sqsubseteq s\\}$. Denote with
$\hat{t}=\mathsf{tp}_{\mathcal{I}_{\mathcal{T},t_{0}}}(h(d))$. The definition
of a homomorphism yields $t\subseteq\hat{t}$. Thus, there is
$\hat{t}^{\prime}\supseteq t^{\prime}$ such that
$\hat{t}\rightsquigarrow_{r}^{\mathcal{T}}\hat{t}^{\prime}$. By definition of
the universal model, $h(d)$ has a $\rho$-successor of type $\hat{t}^{\prime}$
or a $\rho$-predecessor of type $\hat{t}^{\prime\prime}$, for
$\hat{t}^{\prime\prime}\supseteq\hat{t}^{\prime}$. We extend $h$ by setting
$h(d^{\prime})$ to that predecessor or successor, respectively.

After the extension, $h$ witnesses
$(\mathcal{J}_{i+1},d_{i+1})\to(\mathcal{I}_{\mathcal{T},t_{0}},e_{0})$.

Case 2. Application of (R) has added a predecessor $d^{\prime}$ to $d$. Then
$d_{i}=d$ and $d_{i+1}=d^{\prime}$. Let
$t=\mathsf{tp}_{\mathcal{J}_{i+1}}(d)$,
$t^{\prime}=\mathsf{tp}_{\mathcal{J}_{i+1}}(d^{\prime})$ and
$\rho=\\{r\mid(d^{\prime},d)\in r^{\mathcal{J}}\\}$. By construction of the
universal model, there is $r\in\rho$ with
$t^{\prime}\rightsquigarrow_{r}^{\mathcal{T}}t$ and
$\rho=\\{s\mid\mathcal{T}\models r\sqsubseteq s\\}$. Let $e_{0}$ be as in
(ii), that is,
$\hat{t}^{\prime}:=\mathsf{tp}_{\mathcal{I}_{\mathcal{T},t_{0}}}(e_{0})\supseteq
t^{\prime}$. We then have that $\hat{t}^{\prime}\rightsquigarrow_{r}\hat{t}$
for some $\hat{t}\supseteq t$. By definition of the universal model, $e_{0}$
has a $\rho$-successor of type $\hat{t}$ or a $\rho$-predecessor of type
$\hat{t}^{\prime\prime}\supseteq t$. Let this element be $\overline{e}_{0}$.
By induction hypothesis, there is a homomorphism
$h:(\mathcal{J}_{i},d)\to(\mathcal{I}_{\mathcal{T},t_{0}},\overline{e}_{0})$.
We extend $h$ by first setting $h(d^{\prime})=e_{0}$ and then extending $h$ to
all successors of $d$ as in Case 1.

It is not difficult to verify that $h$ witnesses
$(\mathcal{J}_{i+1},d_{i+1})\to(\mathcal{I}_{\mathcal{T},t_{0}},e_{0})$.  ❏

We now use Lemma 22 to develop the mosaic based decision procedure that
underlies the proof of Theorem 21. The main idea is that since we cannot
compute $\mathsf{mod}_{\omega}(\mathcal{T},t_{1})$ explicitly, we decompose
the interpretations in this class into $1$-neighborhoods, of which there are
only finitely many. Such a 1-neighborhood is then represented by a mosaic,
together with a decoration with sets of $\mathcal{T}_{2}$-types that can be
homomorphically embedded into that neighborhood.

Let $\mathcal{T}_{1},\mathcal{T}_{2}$ be $\text{Horn-}{\cal{\cal ALCHIF}}$
TBoxes, $t_{1}$ a $\mathcal{T}_{1}$-type, and $\mathbf{S}$ a signature. We
denote with $\mathsf{rol}(\mathcal{T}_{i})$ the set of all roles $r,r^{-}$
such that the role name $r$ occurs in $\mathcal{T}_{i}$ (possibly as an
inverse role). Moreover, for a set of roles $\rho$ and a signature
$\mathbf{S}$, denote with $\rho|_{\mathbf{S}}$ the restriction of $\rho$ to
$\mathbf{S}$-roles, and with $\rho^{-}$ the set $\\{r^{-}\mid r\in\rho\\}$.

Formally, a _mosaic_ is a tuple $M=(t^{-},\rho,t,S,\ell)$ such that
$(t^{-},\rho,t,S)=n_{1}^{\mathcal{I}_{\mathcal{T}_{1},t_{1}}}(d)$ for some
$d\in\Delta^{\mathcal{I}_{\mathcal{T}_{1},t_{1}}}$ and $\ell:\\{t^{-},t\\}\cup
S\to 2^{\mathsf{tp}(\mathcal{T}_{2})}$ satisfies the following condition:

  1. (M)

For all $\widehat{t}\in\ell(t)$ we have $\widehat{t}\cap\mathbf{S}\subseteq t$
and, for all $\widehat{t}^{\prime}\in\mathsf{tp}(\mathcal{T}_{2})$ and
$r\in\mathsf{rol}(\mathcal{T}_{2})$ with
$\widehat{t}\rightsquigarrow_{r}^{\mathcal{T}_{2}}\widehat{t^{\prime}}$, one
of the following holds for
$\sigma=\\{s\in\mathsf{rol}(\mathcal{T}_{2})\mid\mathcal{T}_{2}\models
r\sqsubseteq s\\}$:

    1. (a)

$\sigma|_{\mathbf{S}}=\emptyset$;

    2. (b)

$t^{-}\neq\bot$, for every $s\in\sigma|_{\mathbf{S}}$ we have $s^{-}\in\rho$,
and $\widehat{t^{\prime}}\in\ell(t^{-})$;

    3. (c)

there is $(\rho^{\prime},t^{\prime})\in S$ with
$\widehat{t^{\prime}}\in\ell(\rho^{\prime},t^{\prime})$ and
$\sigma|_{\mathbf{S}}\subseteq\rho^{\prime}$.

To ease notation, we use $t^{-}_{M}$ to denote $t^{-}$, $\rho_{M}$ to denote
$\rho$, and likewise for the other components of a mosaic $M$. We further use
$\mathcal{M}$ to denote the set of all mosaics.

We now describe an elimination algorithm in the style of Pratt’s type
elimination for PDL (?), but working on mosaics rather than on types; the
existence of this algorithm will establish Theorem 21. Let
$\mathcal{M}^{\prime}\subseteq\mathcal{M}$ be a set of mosaics. An
$M\in\mathcal{M}^{\prime}$ is _good in_ $\mathcal{M}^{\prime}$ if the
following conditions are satisfied:

  1. 1.

for each $(\rho,t)\in S_{M}$, there is an $N\in\mathcal{M}^{\prime}$ such that
$(t_{M},\rho,t)=(t^{-}_{N},\rho_{N},t_{N})$,
$\ell_{M}(\rho,t)=\ell_{N}(t_{N})$, and $\ell_{M}(t_{M})=\ell_{N}(t^{-}_{N})$;

  2. 2.

if $t^{-}_{M}\neq\bot$, there is $N\in\mathcal{M}^{\prime}$ with
$(\rho_{M},t_{M})\in S_{N}$, $t^{-}_{M}=t_{N}$,
$\ell_{M}(t^{-}_{M})=\ell_{N}(t_{N})$, and
$\ell_{M}(t_{M})=\ell_{N}(\rho_{M},t_{M})$.

Our algorithm computes the sequence $\mathcal{M}_{0},\mathcal{M}_{1},\dots$
that starts with $\mathcal{M}_{0}=\mathcal{M}$ and where $\mathcal{M}_{i+1}$
is obtained from $\mathcal{M}_{i}$ by removing all mosaics that are not good
in $\mathcal{M}_{i}$. This sequence eventually stabilizes, say at
$\mathcal{M}_{p}$. The following lemma establishes the central property of the
elimination algorithm.

###### Lemma 23

Let $t_{2}\in\mathsf{tp}(\mathcal{T}_{2})$. Then the following two statements
are equivalent:

  1. 1.

there is a $\mathcal{J}\in\mathsf{mod}_{\omega}(\mathcal{T}_{1},t_{1})$ such
that
$\mathcal{I}_{\mathcal{T}_{2},t_{2}}|^{\mathsf{con}}_{\mathbf{S}}\rightarrow_{\mathbf{S}}\mathcal{J}$;

  2. 2.

$\mathcal{M}_{p}$ contains a mosaic $M$ with $t_{2}\in\ell_{M}(t_{M})$.

Proof.  $1\Rightarrow 2$. Let $h$ be an $\mathbf{S}$-homomorphism from
$\mathcal{I}_{\mathcal{T}_{2},t_{2}}|_{\mathbf{S}}^{\mathsf{con}}$ to some
$\mathcal{J}\in\mathsf{mod}_{\omega}(\mathcal{T}_{1},t_{1})$. For every
$d\in\Delta^{\mathcal{J}}$, denote with $T_{h}(d)$ the set of all types mapped
to $d$ by $h$, that is,

$T_{h}(d)=\big{\\{}\mathsf{tp}_{\mathcal{I}_{\mathcal{T}_{2},t_{2}}}(e)\mid
h(e)=d,~{}e\in\Delta^{\mathcal{I}_{\mathcal{T}_{2},t_{2}}|^{\mathsf{con}}_{\mathbf{S}}}\>\\!\big{\\}}.$

For every element $d\in\Delta^{\mathcal{J}}$, we define a tuple
$M(d)=(t^{-},\rho,t,S,\ell)$ as follows:

  * •

$(t^{-},\rho,t,S)=n_{1}^{\mathcal{J}}(d)$;

  * •

$\ell(t)=T_{h}(d)$;

  * •

if there is a predecessor $d^{\prime}$ of $d$, then
$\ell(t^{-})=T_{h}(d^{\prime})$; otherwise, set $\ell(t^{-})=\emptyset$ (or
any other value);

  * •

for every $(\rho,t^{\prime})\in S$, let $d^{\prime}$ be the $\rho$-successor
of $d$ with $\mathsf{tp}_{\mathcal{J}}(d^{\prime})=t^{\prime}$, and set
$\ell(\rho^{\prime},t^{\prime})=T_{h}(d^{\prime})$.

It is easy to verify that every $M(d)$ obtained in this way is indeed a
mosaic. In particular, it follows from the definition of $\mathcal{J}$ that
$(t^{-},\rho,t,S)=n_{1}^{\mathcal{I}_{\mathcal{T}_{1},t_{1}}}(d^{\prime})$ for
some $d^{\prime}\in\Delta^{\mathcal{I}_{\mathcal{T}_{1},t_{1}}}$. Moreover, by
the fact that $h$ is a homomorphism, Condition (M) is satisfied.

Let $\mathcal{M}(\mathcal{J})=\\{M(d)\mid d\in\Delta^{\mathcal{J}}\\}$. It
follows from the construction that all mosaics in $\mathcal{M}(\mathcal{J})$
are good in $\mathcal{M}(\mathcal{J})$; hence
$\mathcal{M}(\mathcal{J})\subseteq\mathcal{M}_{p}$. Finally, let $d_{0}$ be
the root of $\mathcal{I}_{\mathcal{T}_{2},t_{2}}$ and let $M:=M(h(d_{0}))$.
Then $t_{2}\in\ell_{M}(t_{M})$ and thus Point 2 of Lemma 23 is satisfied.

$2\Leftarrow 1$. Assume that $\mathcal{M}_{p}$ contains a mosaic $M$ with
$t_{2}\in\ell_{M}(t_{M})$. We construct an interpretation $\mathcal{J}$ by
stitching together mosaics. Throughout the construction, we maintain a partial
function $q:\Delta^{\mathcal{J}}\to\mathcal{M}_{p}$ that records for each
domain element of $\mathcal{J}$ the mosaic that gave rise to it. We also
maintain the following invariant:

$\text{If $q(d)=(t^{-},\rho,t,S,\ell)$, then
}n_{1}^{\mathcal{J}}(d)=(t^{-},\rho,t,S).$ ($\ast$)

We start with defining $\mathcal{J}$ as the interpretation corresponding to
the 1-neighborhood represented by $M$ (in the obvious way), and define
$q(e_{0})=M$, where $e_{0}$ is the domain element that corresponds to the
center of that 1-neighborhood. By definition, the invariant ($\ast$ ‣ 4.1) is
satisfied. Then extend $\mathcal{J}$ by doing the following exhaustively in a
fair way: Choose some $d\in\mathcal{J}$ such that $q(d)$ is undefined, and

  * (b)

If $d$ has a predecessor $d^{\prime}$ such that $q(d^{\prime})=M^{\prime}$
then, due to ($\ast$ ‣ 4.1), there is $(\rho,t)\in S_{M^{\prime}}$ such that
$d$ is the $\rho$-successor of $d^{\prime}$ in $\mathcal{J}$ and
$\mathsf{tp}_{\mathcal{J}}(d)=t$. Let $N\in\mathcal{M}_{p}$ be the mosaic that
exists according to Condition 1 of being good for $(\rho,t)\in
S_{M^{\prime}}$. Then extend $\mathcal{J}$ such that
$n_{1}^{\mathcal{J}}(d)=(t^{-}_{N},\rho_{N},t_{N},S_{N})$ and set $q(d)=N$.

  * (c)

If $d$ has a successor $d^{\prime}$ such that $q(d^{\prime})=M^{\prime}$ then,
due to ($\ast$ ‣ 4.1), we know that
$t^{-}_{M^{\prime}}=\mathsf{tp}_{\mathcal{J}}(d)\neq\bot$. Let
$N\in\mathcal{M}_{p}$ be the mosaic that exists according to Condition 2 of
being good. Then extend $\mathcal{J}$ such that
$n_{1}^{\mathcal{J}}(d)=(t^{-}_{N},\rho_{N},t_{N},S_{N})$ and set $q(d)=N$.

It is immediate from the construction that this preserves ($\ast$ ‣ 4.1), and
that one of (a) and (b) always applies. Moreover, by construction, any
interpretation $\mathcal{J}$ obtained in the limit of this process is an
element of $\mathsf{mod}_{\omega}(\mathcal{T}_{1},t_{1})$.

It thus remains to construct an $\mathbf{S}$-homomorphism $h$ that witnesses
$\mathcal{I}_{\mathcal{T}_{2},t_{2}}|^{\mathsf{con}}_{\mathbf{S}}\rightarrow_{\mathbf{S}}\mathcal{J}$.
We construct $h$ step by step, essentially following the construction of
$\mathcal{I}_{\mathcal{T}_{2},t_{2}}$, maintaining the invariant:

If $h(d)$ is defined, then
$\mathsf{tp}_{\mathcal{I}_{\mathcal{T}_{2},t_{2}}}(d)\in\ell_{q(h(d))}(t_{q(h(d))})$.
($\dagger$)

Let $d_{0}$ be the root of $\mathcal{I}_{\mathcal{T}_{2},t_{2}}$. We start
with setting $h(d_{0})=e_{0}$, where $e_{0}$ is as above. By the assumption
that $t_{2}\in\ell_{M}(t_{M})$, invariant ($\dagger$ ‣ 4.1) is satisfied. Now,
exhaustively apply the following step:

Choose
$d\in\Delta^{\mathcal{I}_{\mathcal{T}_{2},t_{2}}|^{\mathsf{con}}_{\mathbf{S}}}$
such that $h(d)$ is not defined but $h(d^{\prime})=e$ is defined for the
predecessor $d^{\prime}$ of $d$. Let
$t=\mathsf{tp}_{\mathcal{I}_{\mathcal{T}_{2},t_{2}}}(d)$,
$t^{\prime}=\mathsf{tp}_{\mathcal{I}_{\mathcal{T}_{2},t_{2}}}(d^{\prime})$,
and $M^{\prime}=q(d^{\prime})$. By definition of
$\mathcal{I}_{\mathcal{T}_{2},t_{2}}$,
$t^{\prime}\rightsquigarrow_{r}^{\mathcal{T}_{2}}t$ for some
$r\in\mathsf{rol}(\mathcal{T}_{2})$. Let $\sigma=\\{s\mid\mathcal{T}\models
r\sqsubseteq s\\}$. By Invariant ($\dagger$ ‣ 4.1),
$t^{\prime}\in\ell_{M^{\prime}}(t_{M^{\prime}})$. Thus, one of (a) to (c) in
Condition (M) applies. Condition (a) in impossible since
$\sigma|_{\mathbf{S}}\neq\emptyset$ as
$d,d^{\prime}\in\Delta^{\mathcal{I}_{\mathcal{T}_{2},t_{2}}|^{\mathsf{con}}_{\mathbf{S}}}$.
In case of (b), we extend $h$ by setting $h(d)$ to the predecessor of
$h(d^{\prime})$. In case of (c), we extend $h$ by setting $h(d)$ to the
according successor of $h(d^{\prime})$.

Note that $h$ extended like this satisfies the homomorphism conditions and
preserves ($\dagger$ ‣ 4.1) due to the conditions in (b) and (c).  ❏

We now finish the proof of Theorem 21. Due to Lemma 22, we can decide
$\mathcal{I}_{\mathcal{T}_{2},t_{2}}|^{\mathsf{con}}_{\mathbf{S}}\rightarrow^{\mathsf{fin}}_{\mathbf{S}}\mathcal{I}_{\mathcal{T}_{1},t_{1}}$
by checking whether there is a
$\mathcal{J}\in\mathsf{mod}_{\omega}(\mathcal{T}_{1},t_{1})$ with
$\mathcal{I}_{\mathcal{T}_{2},t_{2}}|^{\mathsf{con}}_{\mathbf{S}}\rightarrow_{\mathbf{S}}\mathcal{J}$.
By Lemma 23, this can be done by constructing the described sequence of
mosaics $\mathcal{M}_{0},\mathcal{M}_{1},\dots\mathcal{M}_{p}$ and checking
whether $\mathcal{M}_{p}$ contains a mosaic $M$ with $t_{2}\in T_{M}$.

The time bound stated in Theorem 21 is a consequence of the following
observations. We can compute $\mathcal{M}_{0}$ as follows. First, enumerate
all possible tuples $(t^{-},\rho,t,S)$ with the number of elements in $S$
bounded by $|\mathcal{T}_{1}|$ (since the outdegree of
$\mathcal{I}_{\mathcal{T}_{1},t_{1}}$ is bounded by $|\mathcal{T}_{1}|$). Then
remove those which do not correspond to $1$-neighborhoods in
$\mathcal{I}_{\mathcal{T}_{1},t_{1}}$. Note that this requires computing
$\rightsquigarrow_{r}$ for every $r$, which can be done in time
$2^{p(|\mathcal{T}_{1}|)}$, $p$ a polynomial. Moreover, we have to perform
reachability checks to verify that the tuple $(t^{-},\rho,t,S)$ indeed occurs
as the $1$-neighborhood in $\mathcal{I}_{\mathcal{T}_{1},t_{1}}$. Based on
this set of all tuples, we consider all possible combinations with labelings
$\ell$ and remove those tuples $(t^{-},\rho,t,S,\ell)$ which do not satisfy
(M). It is routine to verify that there are at most
$2^{2^{q(|\mathcal{T}_{2}|\log|\mathcal{T}_{1}|)}}$ many mosaics, for some
polynomial $q$. It remains to note that Conditions 1 and 2 of a mosaic being
good can be checked in time polynomial in the size of the current set of
mosaics $\mathcal{M}_{i}$ and that the maximal number of iterations is
$|\mathcal{M}_{0}|$.

###  4.2 Automata Construction

We now prove the upper bound on CQ entailment stated in Theorem 20 based on
the characterization provided by Theorem 18, using the decision procedure
asserted by Theorem 21 as a black box. Our main tool are alternating two-way
tree automata with counting (2ATAc) which extend alternating automata on
unranked infinite trees as used for example by ? (?) with the ability to
count.

A _tree_ is a non-empty (potentially infinite) set of words
$T\subseteq(\mathbb{N}\setminus 0)^{*}$ closed under prefixes. We assume that
trees are finitely branching, that is, for every $w\in T$, the set $\\{i>0\mid
w\cdot i\in T\\}$ is finite. For $w\in(\mathbb{N}\setminus 0)^{*}$, set
$w\cdot 0:=w$. For $w=n_{0}n_{1}\cdots n_{k}$, we set $w\cdot-1:=n_{0}\cdots
n_{k-1}$. For an alphabet $\Theta$, a _$\Theta$ -labeled tree_ is a pair
$(T,L)$ with $T$ a tree and $L:T\rightarrow\Theta$ a node labeling function.

A _2ATA c_ is a tuple $\mathfrak{A}=(Q,\Theta,q_{0},\delta,\Omega)$ where $Q$
is a finite set of states, $\Theta$ is the input alphabet, $q_{0}\in Q$ is the
initial state, $\delta$ is a transition function, and $\Omega:Q\to\mathbb{N}$
is a priority function. The transition function $\delta$ maps every state $q$
and input letter $a\in\Theta$ to a positive Boolean formula $\delta(q,a)$ over
the truth constants $\mathsf{true}$ and $\mathsf{false}$ and _transition
atoms_ of the form $q$, $\Diamond^{-}q$, $\Box^{-}q$, $\Diamond_{n}q$ and
$\Box_{n}q$. A transition $q$ expresses that a copy of $\mathfrak{A}$ is sent
to the current node in state $q$; $\Diamond^{-}q$ means that a copy is sent in
state $q$ to the predecessor node, which is required to exist; $\Box^{-}q$
means the same except that the predecessor node is not required to exist;
$\Diamond_{n}q$ means that a copy of $q$ is sent to $n$ successors and
$\Box_{n}q$ means that a copy of $q$ is sent to all but $n$ successors. We use
$\Diamond q$ and $\Box q$ to abbreviate $\Diamond_{1}q$ and $\Box_{0}q$,
respectively. The semantics of 2ATAc is given in terms of runs as usual,
details are in Appendix B. We use $L(\mathfrak{A})$ to denote the set of
$\Theta$-labeled trees accepted by $\mathfrak{A}$. It is not hard to show that
2ATAc are closed under intersection and that the intersection automaton can be
constructed in polynomial time (using techniques from, e.g., ?). The
_emptiness problem_ for 2ATAc means to decide, given a 2ATAc $\mathfrak{A}$,
whether $L(\mathfrak{A})=\emptyset$. We assume here that the numbers in
transitions of the form $\Diamond_{n}q$ and $\Box_{n}q$ are encoded in
unary.555For binary encoding, Theorem 24 below includes additionally an
exponential dependence in the _size_ of the largest number appearing in
$\delta$. The following result is obtained via reduction to the emptiness
problem of the more standard alternating parity tree automata on ranked trees
(?), see Appendix B.1 for details.

###### Theorem 24

The emptiness problem for 2ATAc is in ExpTime. More precisely, it can be
solved in time single exponential in the number of states and the maximal
priority, and polynomial in all other components.

To prove the 2ExpTime upper bound for CQ entailment stated in Theorem 20, it
thus suffices to show that given $\text{Horn-}{\cal{\cal ALCHIF}}$ TBoxes
$\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ and signatures $\mathbf{A}$ and
$\mathbf{Q}$, one can construct in time
$2^{2^{p(|\mathcal{T}_{2}|\mathsf{log}|\mathcal{T}_{1}|)}}$ a 2ATAc
$\mathfrak{A}$ with single exponentially many states and both maximal priority
and maximal occurring number one such that $L(\mathfrak{A})\neq\emptyset$ iff
$\mathcal{T}_{1}\not\models_{\mathbf{A},\mathbf{Q}}^{\textup{CQ}}\mathcal{T}_{2}$.
This is what we do in the following.

The desired 2ATAc runs over $\Theta$-labeled trees with
$\Theta=2^{\Theta_{0}}\times 2^{\Theta_{1}}\times 2^{\Theta_{2}}$ where

  * •

$\Theta_{0}=\mathbf{A}\cup\\{r^{-}\mid r\in\mathbf{A}\\}$;

  * •

$\Theta_{i}=\mathsf{sig}(\mathcal{T}_{i})\cup\\{r^{-}\mid
r\in\mathsf{sig}(\mathcal{T}_{i})\\}$ for $i=1,2$.

For a $\Theta$-labeled tree $(T,L)$, we use $L_{i}$, $i\in\\{0,1,2\\}$ to
refer to the $i$-th component of $L$, that is,
$L(n)=(L_{0}(n),L_{1}(n),L_{2}(n))$, for all $n\in T$. The component $L_{0}$
represents a (possibly infinite) ABox

$\mathcal{A}_{L}=\\{A(n)\mid A\in L_{0}(n)\\}\cup\\{r(n\cdot-1,n)\mid
n\neq\varepsilon,r\in L_{0}(n)\\},$

where $r^{-}(a,b)$ is identified with $r(b,a)$. Note that even when
$\mathcal{A}_{L}$ is finite it is not necessarily a tree-shaped ABox as it
might have multi-edges and be disconnected. Components $L_{1}$ and $L_{2}$
represent interpretations $\mathcal{I}_{L,1}=(T,\cdot^{\mathcal{I}_{L,1}})$
and
$\mathcal{I}_{L,2}=(\mathsf{ind}(\mathcal{A}_{L}),\cdot^{\mathcal{I}_{L,2}})$,
where for $i\in\\{1,2\\}$:

$\displaystyle A^{\mathcal{I}_{L,i}}$ $\displaystyle\\!\\!\;=\\!\\!\;\\{n\mid
A\in L_{i}(n)\\}$ $\displaystyle r^{\mathcal{I}_{L,i}}$
$\displaystyle\\!\\!\;=\\!\\!\;\\{(n,n\\!\\!\;\cdot\\!\\!\;-1)\mid
r^{-}\\!\in\\!L_{i}(n)\\}\cup\\{(n\\!\\!\;\cdot\\!\\!\;-1,n)\mid
r\\!\in\\!L_{i}(n)\\}$

Now, let $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ be $\text{Horn-}{\cal{\cal
ALCHIF}}$ TBoxes and let $\mathbf{A}$, $\mathbf{Q}$, and $\mathbf{S}$ be
signatures. The claimed 2ATAc $\mathfrak{A}$ is constructed as the
intersection of the four 2ATAcs
$\mathfrak{A}_{1},\mathfrak{A}_{2},\mathfrak{A}_{3},\mathfrak{A}_{4}$ provided
by the following lemma.

###### Lemma 25

There are 2ATAcs
$\mathfrak{A}_{1},\mathfrak{A}_{2},\mathfrak{A}_{3},\mathfrak{A}_{4}$ such
that:

  * –

$\mathfrak{A}_{1}$ accepts $(T,L)$ iff $\mathcal{A}_{L}$ is finite, tree-
shaped, and $\varepsilon\in\mathsf{ind}(\mathcal{A}_{L})$;

  * –

$\mathfrak{A}_{2}$ accepts $(T,L)$ iff $\mathcal{I}_{L,1}$ is a model of
$\mathcal{A}_{L}$ and $\mathcal{T}_{1}$;

  * –

$\mathfrak{A}_{3}$ accepts $(T,L)$ iff $\mathcal{A}_{L}$ is consistent with
$\mathcal{T}_{2}$, and $\mathcal{I}_{L,2}$ is
$\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}_{L}}$ restricted to
$\mathsf{ind}(\mathcal{A}_{L})$;

  * –

$\mathfrak{A}_{4}$ accepts $(T,L)$ iff Conditions (1) and (2) from Theorem 18
are not both satisfied, when $\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}_{L}}$
is replaced with $\mathcal{I}_{L,2}$.

The number of states of $\mathfrak{A}_{1}$ and $\mathfrak{A}_{2}$ is
polynomial in $|\mathcal{T}_{1}|$ (and independent of $\mathcal{T}_{2}$); the
number of states of $\mathfrak{A}_{3}$ is polynomial in $|\mathcal{T}_{2}|$
(and independent of $\mathcal{T}_{1}$), and the number of states of
$\mathfrak{A}_{4},$ is exponential in $|\mathcal{T}_{2}|$ (and independent of
$\mathcal{T}_{1}$). All automata can be constructed in time
$2^{2^{p(|\mathcal{T}_{2}|\mathsf{log}|\mathcal{T}_{1}|)}}$, $p$ a polynomial
and have maximal priority of one.

It can be verified that indeed $L(\mathfrak{A})\neq\emptyset$ iff
$\mathcal{T}_{1}\not\models_{\mathbf{A},\mathbf{Q}}^{\textup{CQ}}\mathcal{T}_{2}$.
The rest of this section is devoted to proving Lemma 25.

#### Automata $\mathfrak{A}_{1}$ and $\mathfrak{A}_{2}$.

The construction of the automaton $\mathfrak{A}_{1}$ is straightforward and
left to the reader. Also $\mathfrak{A}_{2}$ is easy to construct. It checks
that $\mathcal{I}_{L,1}$ is a model of $\mathcal{A}_{L}$ by synchronizing the
$L_{0}$ and $L_{1}$ components of the input tree and that all statements in
$\mathcal{T}_{1}$ are satisfied by $\mathcal{I}_{L,1}$ by imposing constraints
on the $L_{1}$ component. The latter is particularly simple since
$\mathcal{T}_{1}$ is in normal form. For the sake of completeness and as a
warm up, we present the details. Define
$\mathfrak{A}_{2}=(Q_{2},\Theta,q_{0},\delta_{2},\Omega_{2})$ where

$\displaystyle Q_{2}={}$
$\displaystyle\\{q_{0},q_{\mathcal{A}}\\}\cup\\{q_{\alpha}\mid\alpha\in\mathcal{T}_{1}\\}\cup\\{q_{\rho},\overline{q}_{\rho}\mid\rho\in\Theta_{1}\\}\cup{}$
$\displaystyle\\{q_{r,B},q_{r,B}^{\downarrow},\overline{q}_{r,B},\overline{q}_{r,B}^{\downarrow}\mid\exists
r.B\text{ occurs in }\mathcal{T}_{1}\\},$

and $\Omega_{2}$ assigns $0$ to all states. Here, the transition function
$\delta_{2}$ is given as follows. For $\sigma=(L_{0},L_{1},L_{2})$, set

$\begin{array}[]{rcll}\delta_{2}(q_{0},\sigma)&=&\Box q_{0}\wedge
q_{\mathcal{A}}\wedge\bigwedge_{\alpha\in\mathcal{T}_{1}}q_{\alpha}\\\\[2.84526pt]
\delta_{2}(q_{\mathcal{A}},\sigma)&=&\displaystyle\bigwedge_{\rho\in
L_{0}}q_{\rho}\\\
\delta_{2}(q_{\mathsf{func}(r)},\sigma)&=&(q_{r^{-}}\wedge\Box\overline{q}_{r})\vee(\overline{q}_{r^{-}}\wedge\Box_{1}\overline{q}_{r})\\\\[2.84526pt]
\delta_{2}(q_{r\sqsubseteq s},\sigma)&=&\overline{q}_{r}\vee
q_{s}\\\\[2.84526pt] \delta_{2}(q_{A_{1}\sqcap A_{2}\sqsubseteq
B},\sigma)&=&\overline{q}_{A_{1}}\vee\overline{q}_{A_{2}}\vee
q_{B}\\\\[2.84526pt]
\delta_{2}(q_{A\sqsubseteq\bot},\sigma)&=&\overline{q}_{A}\\\\[2.84526pt]
\delta_{2}(q_{\top\sqsubseteq A},\sigma)&=&q_{A}\\\\[2.84526pt]
\delta_{2}(q_{A\sqsubseteq\exists r.B},\sigma)&=&\overline{q}_{A}\vee
q_{r,B}\\\\[2.84526pt] \delta_{2}(q_{A\sqsubseteq\forall
r.B},\sigma)&=&q_{B}\vee\overline{q}_{r^{-},A}\\\\[2.84526pt]
\delta_{2}(q_{r,B},\sigma)&=&\Diamond
q_{r,B}^{\downarrow}\vee(q_{r^{-}}\wedge\Diamond^{-}q_{B})\\\\[2.84526pt]
\delta_{2}(\overline{q}_{r,B},\sigma)&=&\Box\overline{q}_{r,B}^{\downarrow}\wedge(\overline{q}_{r^{-}}\vee{\Box^{-}}\overline{q}_{B})\\\\[2.84526pt]
\delta_{2}(q_{r,B}^{\downarrow},\sigma)&=&q_{r}\wedge q_{B}\\\\[2.84526pt]
\delta_{2}(\overline{q}_{r,B}^{\downarrow},\sigma)&=&\overline{q}_{r}\vee\overline{q}_{B}.\end{array}$

We further set for all $\rho\in\Theta_{1}$:

$\begin{array}[]{rcll}\delta_{2}(q_{\rho},\sigma)&=&\left\\{\begin{array}[]{ll}\mathsf{true}&\text{if
}\rho\in L_{1}\\\ \mathsf{false}&\text{if }\rho\notin
L_{1}\end{array}\right.\\\\[11.38109pt]
\delta_{2}(\overline{q}_{\rho},\sigma)&=&\left\\{\begin{array}[]{ll}\mathsf{true}&\text{if
}\rho\notin L_{1}\\\ \mathsf{false}&\text{if $\rho\in
L_{1}$.}\end{array}\right.\end{array}$

#### Automaton $\mathfrak{A}_{4}$.

We next consider the automaton $\mathfrak{A}_{4}$ as it is the most
interesting and crucial ingredient to the construction of $\mathfrak{A}$.
Recall that $\mathfrak{A}_{4}$ has to make sure that Conditions (1) and (2)
from Theorem 18 are not both satisfied. It achieves this by verifying that its
input $(T,L)$ is such that there is an $n\in\mathsf{ind}(\mathcal{A}_{L})$ for
which one of the following conditions holds, where
$\mathcal{I}_{\mathcal{T}_{2},L_{2}(n)\cap{\sf N_{C}}}$ is the universal model
of the $\mathcal{T}_{2}$-type $L_{2}(n)\cap{\sf N_{C}}$ and $\mathcal{T}_{2}$:

  1. 1.

there is a $\mathbf{Q}$-role $r$ and an
$n^{\prime}\in\mathsf{ind}(\mathcal{A}_{L})$ such that $(n,n^{\prime})\in
r^{\mathcal{I}_{L,2}}$, but $(n,n^{\prime})\notin r^{\mathcal{I}_{L,1}}$;

  2. 2.

there is no $\mathbf{Q}$-homomorphism from
$\mathcal{I}_{\mathcal{T}_{2},L_{2}(n)\cap{\sf
N_{C}}}|^{\mathsf{con}}_{\mathbf{Q}}$ to $\mathcal{I}_{L,1}$ that maps the
root of $\mathcal{I}_{\mathcal{T}_{2},L_{2}(n)\cap{\sf N_{C}}}$ to $n$;

  3. 3.

there is a $\mathbf{Q}$-subtree $\mathcal{I}$ of
$\mathcal{I}_{\mathcal{T}_{2},L_{2}(n)\cap{\sf N_{C}}}$ satisfying the
following two conditions.

    1. (a)

$\mathcal{I}\not\rightarrow_{\mathbf{Q}}\mathcal{I}_{L,1}$;

    2. (b)

$\mathcal{I}\not\rightarrow_{\mathbf{Q}}^{\mathsf{fin}}\mathcal{I}_{\mathcal{T}_{1},\mathsf{tp}_{\mathcal{I}_{L,1}}(m)}$,
for all $m$ with $L_{0}(m)\neq\emptyset$.

For Condition 3, note that every $\mathbf{Q}$-subtree $\mathcal{I}$ of
$\mathcal{I}_{\mathcal{T}_{2},L_{2}(n)\cap{\sf N_{C}}}$ is of the form
$\mathcal{I}_{\mathcal{T}_{2},t^{\prime}}|^{\mathsf{con}}_{\mathbf{Q}}$ with
$\mathcal{I}_{\mathcal{T}_{2},t^{\prime}}$ the universal model of the
$\mathcal{T}_{2}$-type $t^{\prime}$ satisfied at the root of $\mathcal{I}$ and
$\mathcal{T}_{2}$. For a $\mathcal{T}_{2}$-type $t$, we use
$R_{\mathbf{Q}}(t)$ to denote the set of all types that are realized at the
root of a $\mathbf{Q}$-subtree in the universal model
$\mathcal{I}_{\mathcal{T}_{2},t}$ of $t$ and $\mathcal{T}_{2}$. Then, the
$\mathbf{Q}$-subtrees $\mathcal{I}$ in Condition 3b are exactly the
interpretations
$\mathcal{I}_{\mathcal{T}_{2},t}|^{\mathsf{con}}_{\mathbf{Q}}$, $t\in
R_{\mathbf{Q}}(L_{2}(n)\cap{\sf N_{C}})$. Also note that Condition 3b is
exactly the question addressed by Theorem 21.

The essence of Conditions 2 and 3a is to ensure that there is no
$\mathbf{Q}$-homomorphism from
$\mathcal{I}_{\mathcal{T}_{2},t}|^{\mathsf{con}}_{\mathbf{Q}}$ to
$\mathcal{I}_{L,1}$ that maps the root of $\mathcal{I}_{\mathcal{T}_{2},t}$ to
$n$, for some $\mathcal{T}_{2}$-type $t$ and
$n\in\mathsf{ind}(\mathcal{A}_{L})$ (for Condition 3, one has to consider all
$n\in\mathsf{ind}(\mathcal{A}_{L})$). The automaton verifies this by making
sure that one of the following is true:

  * (i)

there is a concept name from $\mathbf{Q}$ that is true at the root of
$\mathcal{I}_{\mathcal{T}_{2},t}$ but not at $n$ in $\mathcal{I}_{L,1}$;

  * (ii)

there is a $\mathcal{T}_{2}$-type $t^{\prime}$ and a set of
$\mathsf{sig}(\mathcal{T}_{2})$-roles $\rho$ with
$t\rightsquigarrow^{\mathcal{T}_{2}}_{\rho}t^{\prime}$ such that there is no
$\mathbf{Q}$-homomorphism from
$\mathcal{I}_{\mathcal{T}_{2},t^{\prime}}|^{\mathsf{con}}_{\mathbf{Q}}$ to
$\mathcal{I}_{L,1}$ that maps the root to a $\rho$-neighbor of $n$.

Note that this is sufficient since the subtrees of
$\mathcal{I}_{\mathcal{T}_{2},t}$ rooted at $\rho$-successors of the root are
exactly the models $\mathcal{I}_{\mathcal{T}_{2},t^{\prime}}$,
$t\rightsquigarrow^{\mathcal{T}_{2}}_{\rho}t^{\prime}$. Condition (ii) is
recursive in the sense that we are faced with the same conditions that we
started with, only for a different $\mathcal{T}_{2}$-type and element of
$\mathsf{ind}(\mathcal{A})$. We need to ensure that the recursion terminates,
which is achieved by assigning appropriate priorities to states.

The above is implemented as follows. Define
$\mathfrak{A}_{4}=(Q_{4},\Theta,q_{0},\delta_{4},\Omega_{4})$ where

$\displaystyle Q_{4}={}$
$\displaystyle\\{q_{0},q_{1}\\}\cup\\{\overline{q}^{t}_{2},\overline{q}^{t}_{3},\overline{q}^{t}_{3b}\mid
t\in\mathsf{tp}(\mathcal{T}_{2})\\}\cup{}$
$\displaystyle\\{\overline{q}^{\rho,t}_{2},\overline{q}^{\rho,t,\downarrow}_{2}\mid
t\in\mathsf{tp}(\mathcal{T}_{2}),\rho\text{ set of
$\mathsf{sig}(\mathcal{T}_{2})$-roles}\\},$

and $\Omega_{4}$ assigns zero to all states, except for states of the form
$q_{0}$ and $q^{t}_{2}$, $t\in\mathsf{tp}(\mathcal{T}_{2})$, to which it
assigns one. For a $\mathcal{T}_{2}$-type $t$ and set of roles $\rho$, we use
$t|_{\mathbf{Q}}$ and $\rho|_{\mathbf{Q}}$ to denote the restriction of $t$
and $\rho$ to (the elements that only use symbols from) $\mathbf{Q}$. For each
$\sigma=(L_{0},L_{1},L_{2})$, $\delta_{4}$ contains the following transitions:

$\begin{array}[h]{@{}r@{~}c@{~}ll@{}}\delta_{4}(q_{0},\sigma)~{}&=\hfil~{}&\left\\{\begin{array}[]{ll}\Diamond
q_{0}\vee q_{1}\vee\overline{q}_{2}^{L_{2}\cap{\sf
N_{C}}}\vee\bigvee_{t^{\prime}\in\mathsf{R}_{\mathbf{Q}}(L_{2}\cap{\sf
N_{C}})}\overline{q}^{t^{\prime}}_{3}&\text{if }L_{0}\neq\emptyset\\\
\mathsf{false}&\text{otherwise}\end{array}\right.\\\\[11.38109pt]
\delta_{4}(q_{1},\sigma)~{}&=\hfil~{}&\left\\{\begin{array}[]{ll@{}}\mathsf{true}&\text{if
$L_{2}\setminus L_{1}$ contains a $\mathbf{Q}$-role }\\\
\mathsf{false}&\text{otherwise}\end{array}\right.\\\\[11.38109pt]
\delta_{4}(\overline{q}^{t}_{2},\sigma)~{}&=\hfil~{}&\left\\{\begin{array}[]{ll}\mathsf{true}&\text{if
}t|_{\mathbf{Q}}\not\subseteq L_{1}\\\
\bigvee_{t\rightsquigarrow^{\mathcal{T}_{2}}_{\rho}t^{\prime}}\overline{q}^{\rho,t^{\prime}}_{2}&\text{otherwise}\end{array}\right.\\\\[11.38109pt]
\delta_{4}(\overline{q}^{\rho,t}_{2},\sigma)~{}&=\hfil~{}&\left\\{\begin{array}[]{ll}\Box\overline{q}^{\rho,t,\downarrow}_{2}&\text{if
}\rho^{-}|_{\mathbf{Q}}\not\subseteq L_{1}\\\
\Box\overline{q}^{\rho,t,\downarrow}_{2}\wedge\Diamond^{-}\overline{q}^{t}_{2}&\text{if
$\rho^{-}|_{\mathbf{Q}}\subseteq L_{1}$}\end{array}\right.\\\\[14.22636pt]
\delta_{4}(\overline{q}^{\rho,t,\downarrow}_{2},\sigma)~{}&=\hfil~{}&\left\\{\begin{array}[]{ll}\mathsf{true}&\text{if
}\rho|_{\mathbf{Q}}\not\subseteq L_{1}\\\ \overline{q}^{t}_{2}&\text{if
}\rho|_{\mathbf{Q}}\subseteq L_{1}\end{array}\right.\\\\[11.38109pt]
\delta_{4}(\overline{q}^{t}_{3},\sigma)~{}&=\hfil~{}&\Box\overline{q}^{t}_{3}\wedge\Box^{-}\overline{q}^{t}_{3}\wedge\overline{q}^{t}_{2}\wedge\overline{q}^{t}_{3b}\\\\[2.84526pt]
\delta_{4}(\overline{q}^{t}_{3b},\sigma)~{}&=\hfil~{}&\left\\{\begin{array}[]{ll@{}}\mathsf{true}&\text{if
}L_{0}=\emptyset\text{ or
}\mathcal{I}_{\mathcal{T}_{2},t}|^{\mathsf{con}}_{\mathbf{Q}}\not\rightarrow^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},L_{1}\cap\mathsf{N_{C}}}\\\
\mathsf{false}&\text{otherwise}\end{array}\right.\end{array}$

Note that states with index $i\in\\{1,2,3,3b\\}$ are used to enforce Condition
$i$ from above. Also note that bounded homomorphisms are not handled directly
by the automaton. The condition
$\mathcal{I}_{\mathcal{T}_{2},t}|^{\mathsf{con}}_{\mathbf{Q}}\not\rightarrow^{\mathsf{fin}}_{\mathbf{Q}}\mathcal{I}_{\mathcal{T}_{1},L_{1}\cap\mathsf{N_{C}}}$
from the last transition is only needed during the construction of the
automaton, and it can be decided in the required time due to Theorem 21. The
sets $R_{\mathbf{Q}}(t)$ can clearly be computed in single exponential time.

#### Automaton $\mathfrak{A}_{3}$.

Recall that $\mathfrak{A}_{3}$ has to accept an input $(T,L)$ iff
$\mathcal{A}_{L}$ is consistent with $\mathcal{T}_{2}$, and
$\mathcal{I}_{L,2}$ is $\mathcal{I}_{\mathcal{T}_{2},\mathcal{A}_{L}}$
restricted to $\mathsf{ind}(\mathcal{A}_{L})$. The construction requires a few
preliminaries, in particular a characterization of whether
$\mathcal{T},\mathcal{A}\models A(a)$ in terms of derivation trees. Similar
yet slightly different characterizations have been used before (e.g. in ?).

Let $\mathcal{T}$ be a $\text{Horn-}{\cal{\cal ALCHIF}}$ TBox and
$\mathcal{A}$ an ABox. A _derivation tree_ for an assertion $A_{0}(a_{0})$ in
$\mathcal{A}$ w.r.t. $\mathcal{T}$ with $A_{0}\in{\sf N_{C}}$ is a finite
$\mathsf{ind}(\mathcal{A})\times{\sf N_{C}}$-labeled tree $(T,V)$ that
satisfies the following conditions:

  1. 1.

$V(\varepsilon)=(a_{0},A_{0})$;

  2. 2.

if $V(x)=(a,A)$ and neither $A(a)\notin\mathcal{A}$ nor $\top\sqsubseteq
A\in\mathcal{T}$, then one of the following holds:

    1. (i)

$x$ has successors $y_{1},\dots,y_{k}$, $k\geq 1$ with $V(y_{i})=(a,A_{i})$
for $1\leq i\leq k$ and $\mathcal{T}\models A_{1}\sqcap\cdots\sqcap
A_{k}\sqsubseteq A$;

    2. (ii)

$x$ has a single successor $y$ with $V(y)=(b,B)$ and there is an
$B\sqsubseteq\forall r.A\in\mathcal{T}$ and an $s(b,a)\in\mathcal{A}$ such
that $\mathcal{T}\models s\sqsubseteq r$;

    3. (iii)

$x$ has a single successor $y$ with $V(y)=(b,B)$ and there is a
$B\sqsubseteq\exists r.A\in\mathcal{T}$ such that $r(b,a)\in\mathcal{A}$ and
$\mathsf{func}(r)\in\mathcal{T}$.

Item (i) of Point 2 above requires $\mathcal{T}\models A_{1}\sqcap\dotsb\sqcap
A_{n}\sqsubseteq A$ instead of $A_{1}\sqcap A_{2}\sqsubseteq A\in\mathcal{T}$
to ‘shortcut’ parts of the universal model that are generated by existential
restrictions. In fact, elements of the universal model generated by
existential restrictions do never appear in a derivation tree. The main
properties of derivation trees are summarized in the following lemma, proved
in Appendix B.2.

###### Lemma 26

Let $\mathcal{T}$ be a $\text{Horn-}{\cal{\cal ALCHIF}}$ TBox and
$\mathcal{A}$. Then

  1. 1.

if $\mathcal{A}$ is consistent with $\mathcal{T}$, then
$\mathcal{T},\mathcal{A}\models A_{0}(a_{0})$ iff there is a derivation tree
for $A_{0}(a_{0})$ in $\mathcal{A}$ w.r.t. $\mathcal{T}$, for all assertions
$A_{0}(a_{0})$;

  2. 2.

$\mathcal{A}$ is consistent with $\mathcal{T}$ iff the following are
satisfied:

    1. (a)

the ABox $\mathcal{A}_{a}=\\{A(a)\mid\mathcal{T},\mathcal{A}\models A(a)\\}$
is consistent with $\mathcal{T}$, for all $a\in\mathsf{ind}(\mathcal{A})$;

    2. (b)

the relation $\\{(a,b)\mid s(a,b)\in\mathcal{A}\\}$ is a partial function
whenever $\mathsf{func}(s)\in\mathcal{T}$.

We now construct the automaton $\mathfrak{A}_{3}$. It ensures that when a
$\Theta$-labeled tree $(T,L)$ is accepted, then for all
$n\in\mathsf{ind}(\mathcal{A}_{L})$, concept names $A$, and roles $r$:

  1. (i)

$A\in L_{2}(n)$ iff there is a derivation tree for $A(n)$ in
$\mathcal{A}_{L}$;

  2. (ii)

for all $n\neq\varepsilon$, $r\in L_{2}(n)$ iff there is a role $s$ such that
$s(n\cdot-1,n)\in\mathcal{A}_{L}$ and $\mathcal{T}_{2}\models s\sqsubseteq r$.

By Point 1 of Lemma 26, these conditions ensure that the interpretation
$\mathcal{I}_{L,2}$ is the universal model of $\mathcal{T}_{2}$ and
$\mathcal{A}$ restricted to $\mathsf{ind}(\mathcal{A}_{L})$, in case
$\mathcal{A}$ is consistent with $\mathcal{T}_{2}$. Given this, we can verify
consistency of $\mathcal{A}$ with $\mathcal{T}_{2}$ based on Point 2 of Lemma
26, that is, we ensure the following:

  * (iii)

the set $L_{2}(n)\cap\mathsf{N_{C}}$ is consistent with $\mathcal{T}_{2}$, for
all $n\in\mathsf{ind}(\mathcal{A})$;

  * (iv)

the relation $\\{(a,b)\mid s(a,b)\in\mathcal{A}_{L}\\}$ is a partial function
whenever $\mathsf{func}(s)\in\mathcal{T}_{2}$.