AReferences of Appendix

# First Order-Rewritability and Containment of Conjunctive Queries in
Horn Description Logics

Meghyn Bienvenu
CNRS, Univ. Montpellier, Inria, France
<EMAIL_ADDRESS>& Peter Hansen  Carsten Lutz
University of Bremen, Germany
{hansen<EMAIL_ADDRESS>& Frank Wolter
University of Liverpool, UK
<EMAIL_ADDRESS>
###### Abstract

We study FO-rewritability of conjunctive queries in the presence of ontologies
formulated in a description logic between $\mathcal{E\kern-1.00006ptL}$ and
Horn-$\mathcal{SHIF}$, along with related query containment problems. Apart
from providing characterizations, we establish complexity results ranging from
ExpTime via NExpTime to 2ExpTime, pointing out several interesting effects. In
particular, FO-rewriting is more complex for conjunctive queries than for
atomic queries when inverse roles are present, but not otherwise.

##  1 Introduction

When ontologies are used to enrich incomplete and heterogeneous data with a
semantics and with background knowledge Calvanese et al. (2009); Kontchakov et
al. (2013); Bienvenu and Ortiz (2015), efficient query anwering is a primary
concern. Since classical database systems are unaware of ontologies and
implementing new ontology-aware systems that can compete with these would be a
huge effort, a main approach used today is _query rewriting_ : the user query
$q$ and the ontology $\mathcal{O}$ are combined into a new query
$q_{\mathcal{O}}$ that produces the same answers as $q$ under $\mathcal{O}$
(over all inputs) and can be handed over to a database system for execution.
Popular target languages for the query $q_{\mathcal{O}}$ include SQL and
Datalog. In this paper, we concentrate on ontologies formulated in description
logics (DLs) and on rewritability into SQL, which we equate with first-order
logic (FO).

FO-rewritability in the context of query answering under DL ontologies was
first studied in Calvanese et al. (2007). Since FO-rewritings are not
guaranteed to exist when ontologies are formulated in traditional DLs, the
authors introduce the DL-Lite family of DLs specifically for the purpose of
ontology-aware query answering using SQL database systems; in fact, the
expressive power of DL-Lite is seriously restricted, in this way enabling
existence guarantees for FO-rewritings. While DL-Lite is a successful family
of DLs, there are many applications that require DLs with greater expressive
power. The potential non-existence of FO-rewritings in this case is not
necessarily a problem in practical applications. In fact, ontologies emerging
from such applications typically use the available expressive means in a
harmless way in the sense that efficient reasoning is often possible despite
high worst-case complexity. One might thus hope that, in practice, FO-
rewritings can often be constructed also beyond DL-Lite.

This hope was confirmed in Bienvenu et al. (2013); Hansen et al. (2015), which
consider the case where ontologies are formulated in a DL of the
$\mathcal{E\kern-1.00006ptL}$ family Baader et al. (2005) and queries are
atomic queries (AQs) of the form $A(x)$. To describe the obtained results in
more detail, let an ontology-mediated query (OMQ) be a triple
$(\mathcal{T},\Sigma,q)$ with $\mathcal{T}$ a description logic TBox
(representing an ontology), $\Sigma$ an ABox signature (the set of concept and
role names that can occur in the data), and $q$ an actual query. Note that
$\mathcal{T}$ and $q$ might use symbols that do not occur in $\Sigma$; in this
way, the TBox enriches the vocabulary available for formulating $q$. We use
$(\mathcal{L},\mathcal{Q})$ to denote the OMQ language that consists of all
OMQs where $\mathcal{T}$ is formulated in the description logic $\mathcal{L}$
and $q$ in the query language $\mathcal{Q}$. In Bienvenu et al. (2013), FO-
rewritability is characterized in terms of the existence of certain tree-
shaped ABoxes, covering a range of OMQ languages between
$(\mathcal{E\kern-1.00006ptL},\text{AQ})$ and
$(\text{Horn-}\mathcal{SHI},\text{AQ})$. On the one hand, this
characterization is used to clarify the complexity of deciding whether a given
OMQ is FO-rewritable, which turns out to be ExpTime-complete. On the other
hand, it provides the foundations for developing practically efficient and
complete algorithms for computing FO-rewritings. The latter was explored
further in Hansen et al. (2015), where a novel type of algorithm for computing
FO-rewritings of OMQs from $(\mathcal{E\kern-1.00006ptL},\text{AQ})$ is
introduced, crucially relying on the previous results from Bienvenu et al.
(2013). Its evaluation shows excellent performance and confirms the hope that,
in practice, FO-rewritings almost always exist. In fact, rewriting fails in
only 285 out of 10989 test cases.

A limitation of the discussed results is that they concern only AQs while in
many applications, the more expressive conjunctive queries (CQs) are required.
The aim of the current paper is thus to study FO-rewritability of OMQ
languages based on CQs, considering ontology languages between
$\mathcal{E\kern-1.00006ptL}$ and Horn-$\mathcal{SHIF}$. In particular, we
provide characterizations of FO-rewritability in the required OMQ languages
that are inspired by those in Bienvenu et al. (2013) (replacing tree-shaped
ABoxes with a more general form of ABox), and we analyze the complexity of FO-
rewritability using an automata-based approach. While practically efficient
algorithms are out of the scope of this article, we believe that our work also
lays important ground for the subsequent development of such algorithms. Our
approach actually _does_ allow the construction of rewritings, but it is not
tailored towards doing that in a practically efficient way. It turns out that
the studied FO-rewritability problems are closely related to OMQ containment
problems as considered in Bienvenu et al. (2012); Bourhis and Lutz (2016). In
fact, being able to decide OMQ containment allows us to concentrate on
connected CQs when deciding FO-rewritability, which simplifies technicalities
considerably. For this reason, we also study characterizations and the
complexity of query containment in the OMQ languages considered.

Our main complexity results are that FO-rewritability and containment are
ExpTime-complete for OMQ languages between
$(\mathcal{E\kern-1.00006ptL},\text{AQ})$ and
$(\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot},\text{CQ})$ and
2ExpTime-complete for OMQ languages between
$(\mathcal{E\kern-1.00006ptLI},\text{CQ})$ and
$(\text{Horn-}\mathcal{SHIF},\text{CQ})$. The lower bound for containment
applies already when both OMQs share the same TBox. Replacing AQs with CQs
thus results in an increase of complexity by one exponential in the presence
of inverse roles (indicated by $\mathcal{I}$), but not otherwise. Note that
the effect that inverse roles can increase the complexity of querying-related
problems was known from expressive DLs of the ${\cal ALC}$ family Lutz (2008),
but it has not previously been observed for Horn-DLs such as
$\mathcal{E\kern-1.00006ptLI}$ and Horn-$\mathcal{SHIF}$. While 2ExpTime might
appear to be very high complexity, we are fortunately also able to show that
the runtime is double exponential only in the size of the actual queries
(which tends to be very small) while it is only single exponential in the size
of the ontologies. We also show that the complexity drops to NExpTime when we
restrict our attention to _rooted_ CQs, that is, CQs which contain at least
one answer variable and are connected. Practically relevant queries are
typically of this kind.

A slight modification of our lower bounds yields new lower bounds for monadic
Datalog containment. In fact, we close an open problem from Chaudhuri and
Vardi (1994) by showing that containment of a monadic Datalog program in a
rooted CQ is coNExpTime-complete. We also improve the 2ExpTime lower bound for
containment of a monadic Datalog program in a CQ from Benedikt et al. (2012)
by showing that it already applies when the arity of EDB relations is bounded
by two, rule bodies are tree-shaped, and there are no constants (which in this
case correspond to nominals); the existing construction cannot achieve the
latter two conditions simultaneously.

Full proofs are provided at http://www.informatik.uni-
bremen.de/tdki/research/papers.html.

Related work. Pragmatic approaches to OMQ rewriting beyond DL-Lite often
consider Datalog as a target language Rosati (2007); Pérez-Urbina et al.
(2010); Eiter et al. (2012); Kaminski et al. (2014); Trivela et al. (2015).
These approaches might produce a non-recursive (thus FO) rewriting if it
exists, but there are no guarantees. FO-rewritability of OMQs based on
expressive DLs is considered in Bienvenu et al. (2014), and based on
existential rules in Baget et al. (2011). A problem related to ours is whether
_all_ queries are FO-rewritable when combined with a given TBox Lutz and
Wolter (2012); Civili and Rosati (2015). There are several related works in
the area of Datalog; recall that a Datalog program is bounded if and only if
it is FO-rewritable Ajtai and Gurevich (1994). For monadic Datalog programs,
boundedness is known to be decidable Cosmadakis et al. (1988) and 2ExpTime-
complete Benedikt et al. (2015); containment is also 2ExpTime-complete
Cosmadakis et al. (1988); Benedikt et al. (2012). OMQs from
$(\text{Horn-$\mathcal{SHI}$},\text{CQ})$ can be translated to monadic Datalog
with an exponential blowup, functional roles (indicated by $\mathcal{F}$) are
not expressible.

##  2 Preliminaries and Basic Observations

Let ${\sf N_{C}}$ and ${\sf N_{R}}$ be disjoint and countably infinite sets of
_concept_ and _role names_. A _role_ is a role name $r$ or an _inverse role_
$r^{-}$, with $r$ a role name. A _Horn- $\mathcal{SHIF}$ 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. In DLs, ontologies are
formalized as TBoxes. A _Horn- $\mathcal{SHIF}$ TBox_ $\mathcal{T}$ is a
finite set of Horn-$\mathcal{SHIF}$ CIs, _functionality assertions_ ${\sf
func}(r)$, _transitivity assertions_ ${\sf trans}(r)$, and _role inclusions
(RIs)_ $r\sqsubseteq s$, with $r$ and $s$ roles. It is standard to assume that
functional roles are not transitive and neither are transitive roles included
in them (directly or indirectly). We make the slighty stronger assumption that
functional roles do not occur on the right-hand side of role inclusions at
all. This assumption seems natural from a modeling perspective and mainly
serves the purpose of simplifying constructions; all our results can be
extended to the milder standard assumption. An _$\mathcal{ELIHF}_{\bot}$ TBox_
is a _Horn- $\mathcal{SHIF}$ TBox_ that contains neither transitivity
assertions nor disjunctions in CIs, an _$\mathcal{E\kern-1.00006ptLI}$ TBox_
is an $\mathcal{ELIHF}_{\bot}$ TBox that contains neither functionality
assertions nor RIs, and an
$\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot}$TBox is an
$\mathcal{ELIHF}_{\bot}$ TBox that does not contain inverse roles.

An _ABox_ is a finite set of _concept assertions_ $A(a)$ and _role assertions_
$r(a,b)$ where $A$ is a concept name, $r$ a role name, and $a,b$ individual
names from a countably infinite set ${\sf N_{I}}$. We sometimes write
$r^{-}(a,b)$ instead of $r(b,a)$ and use $\mathsf{Ind}(\mathcal{A})$ to denote
the set of all individual names used in $\mathcal{A}$. A _signature_ is a set
of concept and role names. We will often assume that the ABox is formulated in
a prescribed signature, which we then call an _ABox signature_. An ABox that
only uses concept and role names from a signature $\Sigma$ is called a
_$\Sigma$ -ABox_.

The semantics of DLs is given in terms of _interpretations_
$\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_ , assigning to each
$A\in{\sf N_{C}}$ a set $A^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}$ and to
each $r\in{\sf N_{R}}$ a relation
$r^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}$. The
interpretation $C^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}$ of a concept $C$
in $\mathcal{I}$ is defined as usual, see Baader et al. (2003). An
interpretation $\mathcal{I}$ _satisfies_ a CI $C\sqsubseteq D$ if
$C^{\mathcal{I}}\subseteq D^{\mathcal{I}}$, a functionality assertion
$\mathsf{func}(r)$ if $r^{\mathcal{I}}$ is a partial function, a transitivity
assertion ${\sf trans}(r)$ if $r^{\mathcal{I}}$ is transitive, an RI
$r\sqsubseteq s$ if $r^{\mathcal{I}}\subseteq s^{\mathcal{I}}$, a concept
assertion $A(a)$ if $a\in A^{\mathcal{I}}$, and a role assertion $r(a,b)$ if
$(a,b)\in r^{\mathcal{I}}$. We say that $\mathcal{I}$ is a _model of_ a TBox
or an ABox if it satisfies all inclusions and assertions in it. An ABox
$\mathcal{A}$ is _consistent_ with a TBox $\mathcal{T}$ if $\mathcal{A}$ and
$\mathcal{T}$ have a common model. If $\alpha$ is a CI, RI, or functionality
assertion, we write $\mathcal{T}\models\alpha$ if all models of $\mathcal{T}$
satisfy $\alpha$.

A _conjunctive query (CQ)_ takes the form
$q=\exists\mathbf{x}\,\varphi(\mathbf{x},\mathbf{y})$ with
$\mathbf{x},\mathbf{y}$ tuples of variables and $\varphi$ a conjunction of
atoms of the form $A(x)$ and $r(x,y)$ that uses only variables from
$\mathbf{x}\cup\mathbf{y}$. The variables in $\mathbf{y}$ are called _answer
variables_ , the _arity_ of $q$ is the length of $\mathbf{y}$, and $q$ is
_Boolean_ if it has arity zero. An _atomic query (AQ)_ is a conjunctive query
of the form $A(x)$. A _union of conjunctive queries (UCQ)_ is a disjunction of
CQs that share the same answer variables. Ontology-mediated queries (OMQs) and
the notation $(\mathcal{L},\mathcal{Q})$ for OMQ languages were already
defined in the introduction. We generally assume that if a role name $r$
occurs in $q$ and $\mathcal{T}\models s\sqsubseteq r$, then
$\mathsf{trans}(s)\notin\mathcal{T}$. This is common since allowing transitive
roles in the query poses serious additional complications, which are outside
the scope of this paper; see e.g. Bienvenu et al. (2010); Gottlob et al.
(2013).

Let $Q=(\mathcal{T},\Sigma,q)$ be an OMQ, $q$ of arity $n$, $\mathcal{A}$ a
$\Sigma$-ABox and $\mathbf{a}\in\mathsf{Ind}(\mathcal{A})^{n}$. We write
$\mathcal{A}\models Q(\mathbf{a})$ if $\mathcal{I}\models q(\mathbf{a})$ for
all models $\mathcal{I}$ of $\mathcal{T}$ and $\mathcal{A}$. In this case,
$\mathbf{a}$ is a _certain answer_ to $Q$ on $\mathcal{A}$. We use
$\mathsf{cert}(Q,\mathcal{A})$ to denote the set of all certain answers to $Q$
on $\mathcal{A}$.

A first-order query (FOQ) is a first-order formula $\varphi$ constructed from
atoms $A(x)$, $r(x,y)$, and $x=y$; here, concept names are viewed as unary
predicates, role names as binary predicates, and predicates of other arity,
function symbols, and constant symbols are not permitted. We write
$\varphi(\mathbf{x})$ to indicate that the free variables of $\varphi$ are
among $\mathbf{x}$ and call $\mathbf{x}$ the _answer variables_ of $\varphi$.
The number of answer variables is the _arity_ of $\varphi$ and $\varphi$ is
_Boolean_ if it has arity zero. We use $\mathsf{ans}(\mathcal{I},\varphi)$ to
denote the set of answers to the FOQ $\varphi$ on the interpretation
$\mathcal{I}$; that is, if $\varphi$ is $n$-ary, then
$\mathsf{ans}(\mathcal{I},\varphi)$ contains all tuples
$\mathbf{d}\in(\Delta^{\mathcal{I}})^{n}$ with
$\mathcal{I}\models\varphi(\mathbf{d})$. To bridge the gap between certain
answers and answers to FOQs, we sometime view an ABox $\mathcal{A}$ as an
interpretation $\mathcal{I}_{\mathcal{A}}$, defined in the obvious way.

For any syntactic object $O$ (such as a TBox, a query, an OMQ), we use $|O|$
to denote the _size_ of $O$, that is, the number of symbols needed to write it
(concept and role names counted as a single symbol).

######  Definition 1 (FO-rewriting).

An FOQ $\varphi$ is an _FO-rewriting_ of an OMQ $Q=(\mathcal{T},\Sigma,q)$ if
$\mathsf{cert}(Q,\mathcal{A})=\mathsf{ans}(\mathcal{I}_{\mathcal{A}},\varphi)$
for all $\Sigma$-ABoxes $\mathcal{A}$ that are consistent with $\mathcal{T}$
. If there is such a $\varphi$, then $Q$ is _FO-rewritable_.

######  Example 2.

(1) Let $Q_{0}=(\mathcal{T}_{0},\Sigma_{0},q_{0}(x,y))$, where
$\mathcal{T}_{0}=\\{\exists r.A\sqsubseteq A,B\sqsubseteq\forall r.A\\}$,
$\Sigma_{0}=\\{r,A,B\\}$ and $q_{0}(x,y)=B(x)\wedge r(x,y)\wedge A(y)$. Then
$\varphi_{0}(x,y)=B(x)\wedge r(x,y)$ is an FO-rewriting of $Q_{0}$.

We will see in Example 10 that the query $Q_{A}$ obtained from $Q_{0}$ by
replacing $q_{0}(x,y)$ with the AQ $A(x)$ is not FO-rewritable (due to the
unbounded propagation of $A$ via $r$-edges by $\mathcal{T}_{0}$). Thus, an FO-
rewritable OMQ can give raise to AQ ‘subqueries’ that are not FO-rewritable.

(2) Let $Q_{1}=(\mathcal{T}_{1},\Sigma_{1},q_{1}(x))$, where
$\mathcal{T}_{1}=\\{\exists r.\exists r.A\sqsubseteq\exists r.A\\}$,
$\Sigma_{1}=\\{r,A\\}$, and $q_{1}(x)=\exists y(r(x,y)\wedge A(y))$. Then
$Q_{1}$ is not FO-rewritable (see again Example 10), but all AQ subqueries
that $Q_{1}$ gives raise to are FO-rewritable.

The main reasoning problem studied in this paper is to decide whether a given
OMQ $Q=(\mathcal{T},\Sigma,q)$ is FO-rewritable. We assume without loss of
generality that every symbol in $\Sigma$ occurs in $\mathcal{T}$ or in $q$. We
obtain different versions of this problem by varying the OMQ language used.
Note that we have defined FO-rewritability relative to ABoxes that are
consistent with the TBox. It is thus important for the user to know whether
that is the case. Therefore, we also consider FO-rewritability of ABox
inconsistency. More precisely, we say that _ABox inconsistency is FO-
rewritable_ relative to a TBox $\mathcal{T}$ and ABox signature $\Sigma$ if
there is a Boolean FOQ $\varphi$ such that for every $\Sigma$-ABox
$\mathcal{A}$, $\mathcal{A}$ is inconsistent with $\mathcal{T}$ iff
$\mathcal{I}_{\mathcal{A}}\models\varphi()$.

Apart from FO-rewritability questions, we will also study OMQ containment. Let
$Q_{i}=(\mathcal{T}_{i},\Sigma,q_{i})$ be two OMQs over the same ABox
signature. We say that $Q_{1}$ _is contained in_ $Q_{2}$, in symbols
$Q_{1}\subseteq Q_{2}$, if
$\mathsf{cert}(Q_{1},\mathcal{A})\subseteq\mathsf{cert}(Q_{2},\mathcal{A})$
holds for all $\Sigma$-ABoxes $\mathcal{A}$ that are consistent with
$\mathcal{T}_{1}$ and $\mathcal{T}_{2}$.

We now make two basic observations that we use in an essential way in the
remaining paper. We first observe that it suffices to concentrate on
$\mathcal{E\kern-1.00006ptLIHF}\kern-1.99997pt_{\bot}$ TBoxes $\mathcal{T}$ in
_normal form_ , that is, all CIs are of one of the forms
$A\sqsubseteq\bot,A\sqsubseteq\exists r.B,\top\sqsubseteq A,B_{1}\sqcap
B_{2}\sqsubseteq A,\exists r.B\sqsubseteq A$ with $A,B,B_{1},B_{2}$ concept
names and $r$ a role. We use $\mathsf{sig}(\mathcal{T})$ to denote the concept
and role names that occur in $\mathcal{T}$.

######  Proposition 3.

Given a Horn-$\mathcal{SHIF}$ (resp.
$\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot}$) TBox $\mathcal{T}_{1}$
and ABox signature $\Sigma$, one can construct in polynomial time an
$\mathcal{E\kern-1.00006ptLIHF}\kern-1.99997pt_{\bot}$ (resp.
$\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot}$) TBox $\mathcal{T}_{2}$
in normal form such that for every $\Sigma$-ABox $\mathcal{A}$,

  1. 1.

$\mathcal{A}$ is consistent with $\mathcal{T}_{1}$ iff $\mathcal{A}$ is
consistent with $\mathcal{T}_{2}$;

  2. 2.

if $\mathcal{A}$ is consistent with $\mathcal{T}_{1}$, then for any CQ $q$
that does not use symbols from
$\mathsf{sig}(\mathcal{T}_{2})\setminus\mathsf{sig}(\mathcal{T}_{1})$, we have
$\mathsf{cert}(Q_{1},\mathcal{A})=\mathsf{cert}(Q_{2},\mathcal{A})$ where
$Q_{i}=(\mathcal{T}_{i},\Sigma,q)$.

Theorem 3 yields polytime reductions of FO-rewritability in
$(\text{Horn-}\mathcal{SHIF},\mathcal{Q})$ to FO-rewritability in
$(\mathcal{E\kern-1.00006ptLIHF}\kern-1.99997pt_{\bot},\mathcal{Q})$ for any
query language $\mathcal{Q}$, and likewise for OMQ containment and FO-
rewritability of ABox inconsistency. It also tells us that, when working with
$\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot}$ TBoxes, we can assume
normal form. Note that transitioning from
$(\text{Horn-}\mathcal{SHF},\mathcal{Q})$ to
$(\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot},\mathcal{Q})$ is not as
easy as in the case with inverse roles since universal restrictions on the
right-hand side of concept inclusions cannot easily be eliminated; for this
reason, we do not consider $(\text{Horn-}\mathcal{SHF},\mathcal{Q})$. From now
on, we work with TBoxes formulated in
$\mathcal{E\kern-1.00006ptLIHF}\kern-1.99997pt_{\bot}$ or
$\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot}$ and assume without
further notice that they are in normal form.

Our second observation is that, when deciding FO-rewritability, we can
restrict our attention to connected queries provided that we have a way of
deciding containment (for potentially disconnected queries). We use conCQ to
denote the class of all connected CQs.

######  Theorem 4.

Let
$\mathcal{L}\in\\{\mathcal{ELIHF_{\bot}},\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot}\\}$.
Then FO-rewritability in $(\mathcal{L},\text{CQ})$ can be solved in polynomial
time when there is access to oracles for containment in
$(\mathcal{L},\mathcal{Q})$ and for FO-rewritability in
$(\mathcal{L},\text{conCQ})$.

To prove Theorem 4, we observe that FO-rewritability of an OMQ
$Q=(\mathcal{T},\Sigma,q)$ is equivalent to FO-rewritability of all OMQs
$Q=(\mathcal{T},\Sigma,q_{c})$ with $q_{c}$ a maximal connected component of
$q$, excluding certain redundant such components (which can be identified
using containment). Backed by Theorem 4, we generally assume connected queries
when studying FO-rewritability, which allows to avoid unpleasant technical
complications and is a main reason for studying FO-rewritability and
containment in the same paper.

##  3 Main Results

In this section, we summarize the main results established in this paper. We
start with the following theorem.

######  Theorem 5.

FO-rewritability and containment are

  1. 1.

2ExpTime-complete for any OMQ language between
$(\mathcal{E\kern-1.00006ptLI},\text{CQ})$ and
$(\text{Horn-}\mathcal{SHIF},\text{CQ})$, and

  2. 2.

ExpTime-complete for any OMQ language between
$(\mathcal{E\kern-1.00006ptL},\text{AQ})$ and
$(\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot},\text{CQ})$.

Moreover, given an OMQ from $(\text{Horn-}\mathcal{SHIF},\text{CQ})$ that is
FO-rewritable, one can effectively construct a UCQ-rewriting.

Like the subsequent results, Theorem 5 illustrates the strong relationship
between FO-rewritability and containment. Note that inverse roles increase the
complexity of both reasoning tasks. We stress that this increase takes place
only when the actual queries are conjunctive queries, since FO-rewritability
for OMQ languages with inverse roles and atomic queries is in ExpTime Bienvenu
et al. (2013).

The 2ExpTime-completeness result stated in Point 1 of Theorem 5 might look
discouraging. However, the situation is not quite as bad as it seems. To show
this, we state the upper bound underlying Point 1 of Theorem 5 a bit more
carefully.

######  Theorem 6.

Given OMQs $Q_{i}=(\mathcal{T}_{i},\Sigma_{i},q_{i})$, $i\in\\{1,2\\}$, from
$(\text{Horn-}\mathcal{SHIF},\text{CQ})$, it can be decided

  1. 1.

in time $2^{2^{p(|q_{1}|+\mathsf{log}(|\mathcal{T}_{1}|))}}$ whether $Q_{1}$
is FO-rewritable and

  2. 2.

in time
$2^{2^{p(|q_{1}|+|q_{2}|+\mathsf{log}(|\mathcal{T}_{1}|+|\mathcal{T}_{2}|))}}$
whether $Q_{1}\subseteq Q_{2}$,

for some polynomial $p$.

Note that the runtime is double exponential only in the size of the actual
queries $q_{1}$ and $q_{2}$, while it is only single exponential in the size
of the TBoxes $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$. This is good news since
the size of $q_{1}$ and $q_{2}$ is typically very small compared to the sizes
of $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$. For this reason, it can even be
reasonable to assume that the sizes of $q_{1}$ and $q_{2}$ are constant, in
the same way in which the size of the query is assumed to be constant in data
complexity. Note that, under this assumption, Theorem 6 yields ExpTime upper
bounds.

One other way to relativize the seemingly very high complexity stated in Point
1 of Theorem 5 is to observe that the lower bound proofs require the actual
query to be Boolean or disconnected. In practical applications, though,
typical queries are connected and have at least one answer variable. We call
such CQs _rooted_ and use rCQ to denote the class of all rooted CQs. Our last
main result states that, when we restrict our attention to rooted CQs, then
the complexity drops to coNExpTime.

######  Theorem 7.

FO-rewritability and containment are coNExpTime-complete in any OMQ language
between $(\mathcal{E\kern-1.00006ptLI},\text{rCQ})$ and
$(\text{Horn-}\mathcal{SHIF},\text{rCQ})$.

##  4 Semantic Characterization

The upper bounds stated in Theorems 5 and 6 are established in two steps. We
first give characterizations of FO-rewritability in terms of the existence of
certain (almost) tree-shaped ABoxes, and then utilize this characterization to
design decision procedures based on alternating tree automata. The semantic
characterizations are of independent interest.

An ABox $\mathcal{A}$ is _tree-shaped_ if the undirected graph with nodes
${\sf Ind}(\mathcal{A})$ and edges $\\{\\{a,b\\}\mid r(a,b)\in\mathcal{A}\\}$
is acyclic and connected and $r(a,b)\in\mathcal{A}$ implies that (i)
$s(a,b)\notin\mathcal{A}$ for all $s\neq r$ and (ii) $s(b,a)\notin\mathcal{A}$
for all role names $s$. For tree-shaped ABoxes $\mathcal{A}$, we often
distinguish an individual used as the root, denoted with $\rho_{\mathcal{A}}$.
$\mathcal{A}$ is _ditree-shaped_ if the directed graph with nodes ${\sf
Ind}(\mathcal{A})$ and edges $\\{(a,b)\mid r(a,b)\in\mathcal{A}\\}$ is a tree
and $r(a,b)\in\mathcal{A}$ implies (i) and (ii). The (unique) root of a
ditree-shaped ABox $\mathcal{A}$ is also denoted with $\rho_{\mathcal{A}}$.

An ABox $\mathcal{A}$ is a _pseudo tree_ if it is the union of ABoxes
$\mathcal{A}_{0},\dots,\mathcal{A}_{k}$ that satisfy the following conditions:

  1. 1.

$\mathcal{A}_{1},\dots,\mathcal{A}_{k}$ are tree-shaped;

  2. 2.

$k\leq|\mathsf{Ind}(\mathcal{A}_{0})|$;

  3. 3.

$\mathcal{A}_{i}\cap\mathcal{A}_{0}=\\{\rho_{\mathcal{A}_{i}}\\}$ and
$\mathsf{Ind}(\mathcal{A}_{i})\cap\mathsf{Ind}(\mathcal{A}_{j})=\emptyset$,
for $1\leq i<j\leq k$.

We call $\mathcal{A}_{0}$ the _core_ of $\mathcal{A}$ and
$\mathcal{A}_{1},\dots,\mathcal{A}_{k}$ the _trees_ of $\mathcal{A}$. The
_width_ of $\mathcal{A}$ is $|\mathsf{Ind}(\mathcal{A}_{0})|$, its _depth_ is
the depth of the deepest tree of $\mathcal{A}$, and its _outdegree_ is the
maximum outdegree of the ABoxes $\mathcal{A}_{1},\dots,\mathcal{A}_{k}$. For a
pseudo tree ABox $\mathcal{A}$ and $\ell\geq 0$, we write
$\mathcal{A}|_{\leq\ell}$ to denote the restriction of $\mathcal{A}$ to the
individuals whose minimal distance from a core individual is at most $\ell$,
and analogously for $\mathcal{A}|_{>\ell}$. A _pseudo ditree ABox_ is defined
analogously to a pseudo tree ABox, except that
$\mathcal{A}_{1},\dots,\mathcal{A}_{k}$ must be ditree-shaped.

When studying FO-rewritability and containment, we can restrict our attention
to pseudo tree ABoxes, and even to pseudo ditree ABoxes when the TBox does not
contain inverse roles. The following statement makes this precise for the case
of containment. Its proof uses unraveling and compactness.

######  Proposition 8.

Let $Q_{i}=(\mathcal{T}_{i},\Sigma,q_{i})$, $i\in\\{1,2\\}$, be OMQs from
($\mathcal{E\kern-1.00006ptLIHF}\kern-1.99997pt_{\bot}$, CQ). Then
$Q_{1}\not\subseteq Q_{2}$ iff there is a pseudo tree $\Sigma$-ABox
$\mathcal{A}$ of outdegree at most $|\mathcal{T}_{1}|$ and width at most
$|q_{1}|$ that is consistent with both $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$
and a tuple $\mathbf{a}$ from the core of $\mathcal{A}$ such that
$\mathcal{A}\models Q_{1}(\mathbf{a})$ and $\mathcal{A}\not\models
Q_{2}(\mathbf{a})$.

If $Q_{1},Q_{2}$ are from
$(\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot},\text{CQ})$, then we can
find a pseudo ditree ABox with these properties.

We now establish a first version of the announced characterizations of FO-
rewritability. Like Proposition 8, they are based on pseudo tree ABoxes.

######  Theorem 9.

Let $Q=(\mathcal{T},\Sigma,q)$ be an OMQ from
($\mathcal{E\kern-1.00006ptLIHF}\kern-1.99997pt_{\bot}$, conCQ). If the arity
of $q$ is at least one, then the following conditions are equivalent:

  1. 1.

$Q$ is FO-rewritable;

  2. 2.

there is a $k\geq 0$ such that for all pseudo tree $\Sigma$-ABoxes
$\mathcal{A}$ that are consistent with $\mathcal{T}$ and of outdegree at most
$|\mathcal{T}|$ and width at most $|q|$: if $\mathcal{A}\models Q(\mathbf{a})$
with $\mathbf{a}$ from the core of $\mathcal{A}$, then $\mathcal{A}|_{\leq
k}\models Q(\mathbf{a})$;

If $q$ is Boolean, this equivalence holds with (2.) replaced by

  * 2′.

there is a $k\geq 0$ such that for all pseudo tree $\Sigma$-ABoxes
$\mathcal{A}$ that are consistent with $\mathcal{T}$ and of outdegree at most
$|\mathcal{T}|$ and of width at most $|q|$: if $\mathcal{A}\models Q$, then
$\mathcal{A}|_{>0}\models Q$ or $\mathcal{A}|_{\leq k}\models Q$.

If $Q$ is from
$(\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot},\text{conCQ})$, then the
above equivalences hold also when pseudo tree $\Sigma$-ABoxes are replaced
with pseudo ditree $\Sigma$-ABoxes.

The proof of Proposition 8 gives a good intuition of why FO-rewritability can
be characterized in terms of ABoxes that are pseudo trees. In fact, the proof
of “$2\Rightarrow 1$” of Theorem 9 is similar to the proof of Proposition 8.
The proof of “$1\Rightarrow 2$” uses locality arguments in the form of
Ehrenfeucht-Fraïssé games. The following examples further illustrate Theorem
9.

######  Example 10.

(1) Non FO-rewritability of the OMQs $Q_{A}$ and $Q_{1}$ from Example 2 is
shown by refuting Condition 2 in Theorem 9: let
$\mathcal{A}_{k}=\\{r(a_{0},a_{1}),\ldots,r(a_{k},a_{k+1}),A(a_{k+1})\\}$, for
all $k\geq 0$. Then $\mathcal{A}_{k}\models Q(a_{0})$ but
$\mathcal{A}_{k}|_{\leq k}\not\models Q(a_{0})$ for $Q\in\\{Q_{A},Q_{1}\\}$.

(2) Theorem 9 only holds for connected CQs: consider
$Q_{2}=(\mathcal{T}_{2},\Sigma_{2},q_{2})$, where $\mathcal{T}_{2}$ is the
empty TBox, $\Sigma_{2}=\\{A,B\\}$, and $q_{2}=\exists x\exists y(A(x)\wedge
B(y))$. $Q_{2}$ is FO-rewritable ($q_{2}$ itself is a rewriting), but
Condition $2^{\prime}$ does not hold: for
$\mathcal{B}_{k}=\\{A(a_{0}),R(a_{0},a_{1},\ldots,R(a_{k},a_{k+1}),B(a_{k+1})\\}$
we have $\mathcal{B}_{k}\models Q_{2}$ but $\mathcal{B}_{k}|_{>0}\not\models
Q_{2}$ and $\mathcal{B}_{k}|_{\leq k}\not\models Q_{2}$.

(3) The modification $2^{\prime}$ of Condition 2 is needed to characterize FO-
rewritability of Boolean OMQs: obtain $Q_{B}$ from $Q_{2}$ by replacing
$q_{2}$ with $\exists xB(x)$. Then $Q_{B}$ is FO-rewritable, but the ABoxes
$\mathcal{B}_{k}$ show that Condition $2$ does not hold.

Theorem 9 does not immediately suggest a decision procedure for FO-
rewritability since there is no bound on the depth of the pseudo tree ABoxes
$\mathcal{A}$ used. The next result establishes such a bound.

######  Theorem 11.

Let $\mathcal{T}$ be an $\mathcal{E\kern-1.00006ptLIHF}\kern-1.99997pt_{\bot}$
TBox. Then Theorem 9 still holds with the following modifications:

  1. 1.

if $q$ is not Boolean or $\mathcal{T}$ is an
$\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot}$ TBox, “there is a $k\geq
0$” is replaced with “for $k=|q|+2^{4(|\mathcal{T}|+|q|)^{2}}$”;

  2. 2.

if $q$ is Boolean, “there is a $k\geq 0$” is replaced with “for
$k=|q|+2^{4(|\mathcal{T}|+2^{|q|})^{2}}$”.

The proof of Theorem 11 uses a pumping argument based on derivations of
concept names in the pumped ABox by $\mathcal{T}$. Due to the presence of
inverse roles, this is not entirely trivial and uses what we call _transfer
sequences_ , describing the derivation history at a point of an ABox. Together
with the proof of Theorem 9, Theorem 11 gives rise to an algorithm that
constructs actual rewritings when they exist.

##  5 Constructing Automata

We show that Proposition 8 and Theorem 11 give rise to automata-based decision
procedures for containment and FO-rewritability that establish the upper
bounds stated in Theorems 5 and 6. By Theorem 4, it suffices to consider
connected queries in the case of FO-rewritability. We now observe that we can
further restrict our attention to Boolean queries. We use BCQ (resp. conBCQ)
to denote the class of all Boolean CQs (resp. connected Boolean CQs).

######  Lemma 12.

Let
$\mathcal{L}\in\\{\mathcal{ELIHF_{\bot}},\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot}\\}$.
Then

  1. 1.

FO-rewritability in $(\mathcal{L},\text{conCQ})$ can be reduced in polytime to
FO-rewritability in $(\mathcal{L},\text{conBCQ})$;

  2. 2.

Containment in $(\mathcal{L},\text{CQ})$ can be reduced in polytime to
containment in $(\mathcal{L},\text{BCQ})$.

The decision procedures rely on building automata that accept pseudo tree
ABoxes which witness non-containment and non-FO-rewritability as stipulated by
Proposition 8 and Theorem 11, respectively. We first have to encode pseudo
tree ABoxes in a suitable way.

A _tree_ is a non-empty (and potentially infinite) set
$T\subseteq\mathbbm{N}^{*}$ closed under prefixes. We say that $T$ is _$m$
-ary_ if for every $x\in T$, the set $\\{i\mid x\cdot i\in T\\}$ is of
cardinality at most $m$. For an alphabet $\Gamma$, a _$\Gamma$ -labeled tree_
is a pair $(T,L)$ with $T$ a tree and $L:T\rightarrow\Gamma$ a node labeling
function. Let $Q=(\mathcal{T},\Sigma,q)$ be an OMQ from
$(\mathcal{ELIHF}_{\bot},\text{conBCQ})$. We encode pseudo tree ABoxes of
width at most $|q|$ and outdegree at most $|\mathcal{T}|$ by
$(|\mathcal{T}|\cdot|q|)$-ary $\Sigma_{\varepsilon}\cup\Sigma_{N}$-labeled
trees, where $\Sigma_{\varepsilon}$ is an alphabet used for labeling root
nodes and $\Sigma_{N}$ is for non-root nodes.

The alphabet $\Sigma_{\varepsilon}$ consists of all $\Sigma$-ABoxes
$\mathcal{A}$ such that $\mathsf{Ind}(\mathcal{A})$ only contains individual
names from a fixed set $\mathsf{Ind}_{\mathsf{core}}$ of size $|q|$ and
$\mathcal{A}$ satisfies all functionality statements in $\mathcal{T}$. The
alphabet $\Sigma_{N}$ consists of all subsets $\Theta\subseteq({\sf
N_{C}}\cap\Sigma)\uplus\\{r,r^{-}\mid r\in{\sf
N_{R}}\cap\Sigma\\}\uplus\mathsf{Ind}_{\mathsf{core}}$ that contain exactly
one (potentially inverse) role and at most one element of
$\mathsf{Ind}_{\mathsf{core}}$. A $(|\mathcal{T}|\cdot|q|)$-ary
$\Sigma_{\varepsilon}\cup\Sigma_{N}$-labeled tree is _proper_ if (i) the root
node is labeled with a symbol from $\Sigma_{\varepsilon}$, (ii) each child of
the root is labeled with a symbol from $\Sigma_{N}$ that contains an element
of $\mathsf{Ind}_{\mathsf{core}}$, (iii) every other non-root node is labeled
with a symbol from $\Sigma_{N}$ that contains no individual name, and (iv)
every non-root node has at most $|q|$ successors and (v) for every
$a\in\mathsf{Ind}_{\mathsf{core}}$, the root node has at most $|q|$ successors
whose label includes $a$.

A proper $\Sigma_{\varepsilon}\cup\Sigma_{N}$-labeled tree $(T,L)$ represents
a pseudo tree ABox $\mathcal{A}_{(T,L)}$ whose individuals are those in the
ABox $\mathcal{A}$ that labels the root of $T$ plus all non-root nodes of $T$,
and whose assertions are

$\begin{array}[]{l}\mathcal{A}\cup\\{A(x)\mid A\in L(x)\\}\\\\[1.42262pt]
\cup\;\\{r(b,x)\mid\\{b,r\\}\subseteq
L(x)\\}\cup\\{r(x,b)\mid\\{b,r^{-}\\}\subseteq L(x)\\}\\\\[1.42262pt]
\cup\;\\{r(x,y)\mid r\in L(y),y\text{ is a child of
}x,L(x)\in\Sigma_{N}\\}\\\\[1.42262pt] \cup\;\\{r(y,x)\mid r^{-}\in
L(y),y\text{ is a child of }x,L(x)\in\Sigma_{N}\\}.\end{array}$

As the automaton model, we use two-way alternating parity automata on finite
trees (TWAPAs). As usual, $L(\mathfrak{A})$ denotes the tree language accepted
by the TWAPA $\mathfrak{A}$. Our central observation is the following.

######  Proposition 13.

For every OMQ $Q=(\mathcal{T},\Sigma,q)$ from
$(\mathcal{ELIHF}_{\bot},\text{BCQ})$, there is a TWAPA

  1. 1.

$\mathfrak{A}_{Q}$ that accepts a $(|\mathcal{T}|\cdot|q|)$-ary
$\Sigma_{\varepsilon}\cup\Sigma_{N}$-labeled tree $(T,L)$ iff it is proper,
$\mathcal{A}_{(T,L)}$ is consistent with $\mathcal{T}$ , and
$\mathcal{A}_{(T,L)}\models Q$;

$\mathfrak{A}_{Q}$ has at most $2^{p(|q|+\mathsf{log}(|\mathcal{T}|))}$
states, and at most $p(|q|+|\mathcal{T}|)$ states if $\mathcal{T}$ is an
$\mathcal{ELHF}_{\bot}$ TBox, $p$ a polynomial.

  2. 2.

$\mathfrak{A}_{\mathcal{T}}$ that accepts a $(|\mathcal{T}|\cdot|q|)$-ary
$\Sigma_{\varepsilon}\cup\Sigma_{N}$-labeled tree $(T,L)$ iff it is proper and
$\mathcal{A}_{(T,L)}$ is consistent with $\mathcal{T}$.

$\mathfrak{A}_{\mathcal{T}}$ has at most $p(|\mathcal{T}|)$ states, $p$ a
polynomial.

We can construct $\mathfrak{A}_{Q}$ and $\mathfrak{A}_{\mathcal{T}}$ in time
polynomial in their size.

The construction of the automata in Proposition 13 uses forest decompositions
of the CQ $q$ as known for example from Lutz (2008). The difference in
automata size between $\mathcal{ELIHF}_{\bot}$ and $\mathcal{ELHF}_{\bot}$ is
due to the different number of tree-shaped subqueries that can arise in these
decompositions.

To decide $Q_{1}\subseteq Q_{2}$ for OMQs
$Q_{i}=(\mathcal{T}_{i},\Sigma,q_{i})$, $i\in\\{1,2\\}$, from
$(\mathcal{ELIHF}_{\bot},\text{BCQ})$, by Proposition 8 it suffices to decide
whether $L(\mathfrak{A}_{Q_{1}})\cap
L(\mathfrak{A}_{\mathcal{T}_{2}})\subseteq L(\mathfrak{A}_{Q_{2}})$. Since
this question can be polynomially reduced to a TWAPA emptiness check and the
latter can be executed in time single exponential in the number of states,
this yields the upper bounds for containment stated in Theorems 5 and 6.

To decide non-FO-rewritability of an OMQ $Q=(\mathcal{T},\Sigma,q)$ from
$(\mathcal{ELIHF}_{\bot},\text{conBCQ})$, by Theorem 11 we need to decide
whether there is a pseudo tree $\Sigma$-ABox $\mathcal{A}$ of outdegree at
most $|\mathcal{T}|$ and width at most $|q|$ that is consistent with
$\mathcal{T}$ and satisfies (i) $\mathcal{A}\models Q$, (ii)
$\mathcal{A}|_{>0}\not\models Q$, and (iii) $\mathcal{A}|_{\leq k}\not\models
Q$ where $k=|q|+2^{4(|\mathcal{T}|+2^{|q|})^{2}}$. For consistency with
$\mathcal{T}$ and for (i), we use the automaton $\mathfrak{A}_{Q}$ from
Proposition 13. To achieve (ii) and (iii), we amend the tree alphabet
$\Sigma_{\varepsilon}\cup\Sigma_{n}$ with additional labels that implement a
counter which counts up to $k$ and annotate each node in the tree with its
depth (up to $k$). We then complement $\mathfrak{A}_{Q}$ (which for TWAPAs can
be done in polynomial time), relativize the resulting automaton to all but the
first level of the input ABox for (ii) and to the first $k$ levels for (iii),
and finally intersect all automata and check emptiness. This yields the upper
bounds for FO-rewritability stated in Theorems 5 and 6.

As remarked in the introduction, apart from FO-rewritability of an OMQ
$(\mathcal{T},\Sigma,q)$ we should also be interested in FO-rewritability of
ABox inconsistency relative to $\mathcal{T}$ and $\Sigma$. We close this
section with noting that an upper bound for this problem can be obtained from
Point 2 of Proposition 13 since TWAPAs can be complemented in polynomial time.
A matching lower bound can be found in Bienvenu et al. (2013).

######  Theorem 14.

In $\mathcal{ELIHF}_{\bot}$, FO-rewritability of ABox inconsistency is
ExpTime-complete.

##  6 Rooted Queries and Lower Bounds

We first consider the case of rooted queries and establish the upper bound in
Theorem 7.

######  Theorem 15.

FO-rewritability and containment in $(\mathcal{ELIHF}_{\bot},\text{rCQ})$ are
in coNExpTime.

Because of space limitations, we confine ourselves to a brief sketch,
concentrating on FO-rewritability. By Point 1 of Theorem 11, deciding non-FO-
rewritability of an OMQ $Q=(\mathcal{T},\Sigma,q)$ from
$(\mathcal{ELIHF}_{\bot},\text{rCQ})$ comes down to checking the existence of
a pseudo tree $\Sigma$-ABox $\mathcal{A}$ that is consistent with
$\mathcal{T}$ and such that $\mathcal{A}\models Q(\mathbf{a})$ and
$\mathcal{A}|_{\leq k}\not\models Q(\mathbf{a})$ for some tuple of individuals
$\mathbf{a}$ from the core of $\mathcal{A}$, for some suitable $k$. Recall
that $\mathcal{A}\models Q(\mathbf{a})$ if and only if there is a homomorphism
$h$ from $q$ to the pseudo tree-shaped canonical model of $\mathcal{T}$ and
$\mathcal{A}$ that takes the answer variables to $\mathbf{a}$. Because
$\mathbf{a}$ is from the core of $\mathcal{A}$ and $q$ is rooted, $h$ can map
existential variables in $q$ only to individuals from $\mathcal{A}|_{|q|}$ and
to the anonymous elements in the subtrees below them. To decide the existence
of $\mathcal{A}$, we can thus guess $\mathcal{A}|_{|q|}$ together with sets of
concept assertions about individuals in $\mathcal{A}|_{|q|}$ that can be
inferred from $\mathcal{A}$ and $\mathcal{T}$, and from $\mathcal{A}|_{\leq
k}$ and $\mathcal{T}$. We can then check whether there is a homomorphism $h$
as described, without access to the full ABoxes $\mathcal{A}$ and
$\mathcal{A}|_{\leq k}$. It remains to ensure that the guessed initial part
$\mathcal{A}_{|q|}$ can be extended to $\mathcal{A}$ such that the entailed
concept assertions are precisely those that were guessed, by attaching tree-
shaped ABoxes to individuals on level $|q|$. This can be done by a mix of
guessing and automata techniques.

We next establish the lower bounds stated in Theorems 5 and 7. For Theorem 5,
we only prove a lower bound for Point 1 as the one in Point 2 follows from
Bienvenu et al. (2013).

######  Theorem 16.

Containment and FO-rewritability are

  1. 1.

coNExpTime-hard in $(\mathcal{E\kern-1.00006ptLI},\text{rCQ})$ and

  2. 2.

2ExpTime-hard in $(\mathcal{E\kern-1.00006ptLI},\text{CQ})$.

The results for containment apply already when both OMQs share the same TBox.

Point 1 is proved by reduction of the problem of tiling a torus of exponential
size, and Point 2 is proved by reduction of the word problem of exponentially
space-bounded alternating Turing machines (ATMs). The proofs use queries
similar to those introduced in Lutz (2008) to establish lower bounds on the
complexity of query answering in the expressive OMQ languages $({\cal
ALCI},\text{rCQ})$ and $({\cal ALCI},\text{CQ})$. A major difference to the
proofs in Lutz (2008) is that we represent torus tilings / ATM computations in
the ABox that witnesses non-containment or non-FO-rewritability, instead of in
the ‘anonymous part’ of the model created by existential quantifiers.

The proof of Point 2 of Theorem 16 can be modified to yield new lower bounds
for monadic Datalog containment. Recall that the rule body of a Datalog
program is a CQ. _Tree-shapedness_ of a CQ $q$ is defined in the same way as
for an ABox in Section 4, that is, $q$ viewed as an undirected graph must be a
tree without multi-edges.

######  Theorem 17.

For monadic Datalog programs which contain no EDB relations of arity larger
than two and no constants, containment

  1. 1.

in a rooted CQ is coNExpTime-hard;

  2. 2.

in a CQ is 2ExpTime-hard, even when all rule bodies are tree-shaped.

Point 1 closes an open problem from Chaudhuri and Vardi (1994), where a
coNExpTime upper bound for containment of a monadic Datalog program in a
rooted UCQ was proved and the lower bound was left open. Point 2 further
improves a lower bound from Benedikt et al. (2012) which also does not rely on
EDB relations of arity larger than two, but requires that rule bodies are not
tree-shaped or constants are present (which, in this case, correspond to
nominals in the DL world).

##  7 Conclusion

A natural next step for future work is to use the techniques developed here
for devising practically efficient algorithms that construct actual
rewritings, which was very successful in the AQ case Hansen et al. (2015).

An interesting open theoretical question is the complexity of FO-rewritability
and containment for the OMQ languages considered in this paper in the special
case when the ABox signature contains all concept and role names.

Acknowledgements. Bienvenu was supported by ANR project PAGODA
(12-JS02-007-01), Hansen and Lutz by ERC grant 647289, Wolter by EPSRC UK
grant EP/M012646/1.

## References

  * Ajtai and Gurevich [1994] Miklós Ajtai and Yuri Gurevich.  Datalog vs First-Order Logic.  J. Comput. Syst. Sci.,49(3): 562–588, 1994.
  * Baader et al. [2003] Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F. Patel-Schneider, editors.  The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, 2003.
  * Baader et al. [2005] Franz Baader, Sebastian Brandt, and Carsten Lutz.  Pushing the $\mathcal{E\kern-1.00006ptL}$ envelope.  In Proc. of IJCAI, pages 364–369, 2005.
  * Baget et al. [2011] Jean-François Baget, Michel Leclère, Marie-Laure Mugnier, and Eric Salvat.  On rules with existential variables: Walking the decidability line.  Artif. Intell., 175(9-10):1620–1654, 2011.
  * Benedikt et al. [2012] Michael Benedikt, Pierre Bourhis, and Pierre Senellart.  Monadic Datalog Containment.  In Proc. of ICALP, pages 79–91, 2012.
  * Benedikt et al. [2015] Michael Benedikt, Balder ten Cate, Thomas Colcombet, and Michael Vanden Boom.  The Complexity of Boundedness for Guarded Logics.  In Proc. of LICS, pages 293–304, 2015.
  * Bienvenu and Ortiz [2015] Meghyn Bienvenu and Magdalena Ortiz.  Ontology-mediated query answering with data-tractable description logics.  In Proc. of Reasoning Web, volume 9203 of LNCS, pages 218–307, 2015.
  * Bienvenu et al. [2010] Meghyn Bienvenu, Thomas Eiter, Carsten Lutz, Magdalena Ortiz, and Mantas Simkus.  Query answering in the description logic S.  In Proc. of DL, volume 573 of CEUR-WS, 2010\.
  * Bienvenu et al. [2012] Meghyn Bienvenu, Carsten Lutz, and Frank Wolter.  Query containment in description logics reconsidered.  In Proc of KR, pages 221–231, 2012.
  * Bienvenu et al. [2013] Meghyn Bienvenu, Carsten Lutz, and Frank Wolter.  First order-rewritability of atomic queries in Horn description logics.  In Proc. of IJCAI, pages 754–760, 2013.
  * Bienvenu et al. [2014] Meghyn Bienvenu, Balder ten Cate, Carsten Lutz, and Frank Wolter.  Ontology-based data access: a study through disjunctive datalog, CSP, and MMSNP.  Proc. of TODS, 39, 2014.
  * Bourhis and Lutz [2016] Pierre Bourhis and Carsten Lutz.  Containment in monadic disjunctive datalog, MMSNP, and expressive description logics.  In Proc. of KR, 2016.
  * Calvanese et al. [2007] Diego Calvanese, Giuseppe De Giacomo, Domenico Lembo, Maurizio Lenzerini, and Riccardo Rosati.  Tractable reasoning and efficient query answering in description logics: The DL-Lite family.  J. Autom. Reasoning, 39(3):385–429, 2007.
  * Calvanese et al. [2009] Diego Calvanese, Giuseppe De Giacomo, Domenico Lembo, Maurizio Lenzerini, Antonella Poggi, Mariano Rodriguez-Muro, and Riccardo Rosati.  Ontologies and databases: The DL-Lite approach.  In Proc. of Reasoning Web, volume 5689 of LNCS, pages 255–356, 2009.
  * Chaudhuri and Vardi [1994] Surajit Chaudhuri and Moshe Y. Vardi.  On the complexity of equivalence between recursive and nonrecursive datalog programs  In Proc. of PODS, pages 107–116, 1994.
  * Civili and Rosati [2015] Cristina Civili and Riccardo Rosati.  On the first-order rewritability of conjunctive queries over binary guarded existential rules.  In Proc. of CILC, volume 1459 of CEUR-WS, pages 25–30, 2015\.
  * Cosmadakis et al. [1988] Stavros S. Cosmadakis, Haim Gaifman, Paris C. Kanellakis, and Moshe Y. Vardi.  Decidable optimization problems for database logic programs (preliminary report).  In Proc. of STOC, pages 477–490, 1988.
  * Eiter et al. [2012] Thomas Eiter, Magdalena Ortiz, Mantas Simkus, Trung-Kien Tran, and Guohui Xiao.  Query rewriting for Horn-SHIQ plus rules.  In Proc. of AAAI, 2012.
  * Gottlob et al. [2013] Georg Gottlob, Andreas Pieris, and Lidia Tendera.  Querying the guarded fragment with transitivity.  In Proc. of ICALP, volume 7966 of LNCS, pages 287–298, 2013\.
  * Hansen et al. [2015] Peter Hansen, Carsten Lutz, Inanç Seylan, and Frank Wolter.  Efficient query rewriting in the description logic EL and beyond.  In Proc. of IJCAI, pages 3034–3040, 2015.
  * Kaminski et al. [2014] Mark Kaminski, Yavor Nenov, and Bernardo Cuenca Grau.  Computing datalog rewritings for disjunctive datalog programs and description logic ontologies.  In Proc. of RR, pages 76–91, 2014.
  * Kontchakov et al. [2013] Roman Kontchakov, Mariano Rodriguez-Muro, and Michael Zakharyaschev.  Ontology-based data access with databases: A short course.  In Proc. of Reasoning Web, pages 194–229, 2013.
  * Lutz and Wolter [2012] Carsten Lutz and Frank Wolter.  Non-uniform data complexity of query answering in description logics.  In Proc. of KR, 2012.
  * Lutz [2008] Carsten Lutz.  The complexity of conjunctive query answering in expressive description logics.  In Proc. of IJCAR, volume 5195 of LNCS, pages 179–193, 2008\.
  * Pérez-Urbina et al. [2010] Héctor Pérez-Urbina, Boris Motik, and Ian Horrocks.  Tractable query answering and rewriting under description logic constraints.  J. Applied Logic, 8(2):186–209, 2010.
  * Rosati [2007] Riccardo Rosati.  On conjunctive query answering in EL.  In Proc. of DL, pages 451–458, 2007.
  * Trivela et al. [2015] Despoina Trivela, Giorgos Stoilos, Alexandros Chortaras, and Giorgos B. Stamou.  Optimising resolution-based rewriting algorithms for OWL ontologies.  J. Web Sem., 33:30–49, 2015.

Appendix

##  Appendix A Proofs for Section 2

See 3

###### Proof.

The proof is similar to reductions provided in
journals/jar/HustadtMS07,conf/ijcai/Kazakov09. We sketch the proof for
Horn-$\mathcal{SHIF}$. The proof for
$\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot}$is similar and omitted.

Assume a $\mathcal{SHIF}$ TBox $\mathcal{T}$ is given. The following rules are
used to rewrite $\mathcal{T}$ into an $\mathcal{ELIHF}_{\bot}$ TBox in normal
form. It then only remains to eliminate the transitivity assertions. We assume
that the concept names introduced in the rules below are fresh (not in ${\sf
sig}(\mathcal{T})\cup\Sigma$):

  * •

If $L$ is of the form $L_{1}\sqcap L_{2}$ and $R$ is not a concept name, then
take a fresh concept name $A$ and replace $L\sqsubseteq R$ by $L\sqsubseteq A$
and $A\sqsubseteq R$. If $R$ is a concept name, and either $L_{1}$ or $L_{2}$
are not concept names, then take fresh concept names $A_{1},A_{2}$ and replace
$L\sqsubseteq R$ by $L_{1}\sqsubseteq A_{1}$, $L_{2}\sqsubseteq A_{2}$ and
$A_{1}\sqcap A_{2}\sqsubseteq R$;

  * •

If $L$ is of the form $L_{1}\sqcup L_{2}$ and $R$ is a concept name, then
replace $L\sqsubseteq R$ by $L_{1}\sqsubseteq R$ and $L_{2}\sqsubseteq R$.
Otherwise take a fresh concept name $A$ and replace $L\sqsubseteq R$ by
$L\sqsubseteq A$ and $A\sqsubseteq R$;

  * •

If $L$ is of the form $\exists r.L^{\prime}$ and $L^{\prime}$ is not a concept
name, then take a fresh concept name $A^{\prime}$ and replace $L\sqsubseteq R$
by $L^{\prime}\sqsubseteq A^{\prime}$ and $\exists r.A^{\prime}\sqsubseteq R$;

  * •

If $R$ is of the form $\neg A$, then replace $L\sqsubseteq R$ by $L\sqcap
A\sqsubseteq\bot$;

  * •

If $R$ is of the form $R_{1}\sqcap R_{2}$ and $L$ is not a concept name, then
take a fresh concept name $A$ and replace $L\sqsubseteq R$ by $L\sqsubseteq A$
and $A\sqsubseteq R$. Otherwise take fresh concept names $A_{1},A_{2}$ and
replace $L\sqsubseteq R$ by $L\sqsubseteq A_{1}$, $L\sqsubseteq A_{2}$,
$A_{1}\sqsubseteq R_{1}$, and $A_{2}\sqsubseteq R_{2}$;

  * •

If $R$ is of the form $\neg L^{\prime}\sqcup R^{\prime}$, then replace
$L\sqsubseteq R$ by $L\sqcap L^{\prime}\sqsubseteq R^{\prime}$;

  * •

If $R$ is of the form $\exists r.R^{\prime}$ and $R^{\prime}$ is not a concept
name, then take a fresh concept name $A^{\prime}$ and replace $L\sqsubseteq R$
by $L\sqsubseteq\exists r.A^{\prime}$ and $A^{\prime}\sqsubseteq R^{\prime}$;

  * •

If $R$ is of the form $\forall r.R^{\prime}$, then replace $L\sqsubseteq R$ by
$\exists r^{-}.L\sqsubseteq R$.

The resulting TBox $\mathcal{T}^{\prime}$ is a conservative extension of
$\mathcal{T}$; i.e., it has the following two properties:

  * •

$\mathcal{T}^{\prime}\models\mathcal{T}$;

  * •

every model $\mathcal{I}$ of $\mathcal{T}$ can be extended to a model of
$\mathcal{T}^{\prime}$ by appropriately interpreting the fresh concept names.

Now we show how transitivity assertions can be eliminated from
$\mathcal{T}^{\prime}$: for any role $r$ with $\mathcal{T}\models{\sf
trans}(r)$ and concept name $B$ take a fresh concept name $X$ and add the CIs
$\exists r.B\sqsubseteq X$, $\exists r.X\sqsubseteq X$, and
$X\sqsubseteq\exists r.B$ to $\mathcal{T}^{\prime}$. Also remove the
transitivity assertions from $\mathcal{T}^{\prime}$. The resulting TBox,
$\mathcal{T}^{\prime\prime}$, is an $\mathcal{ELIHF}_{\bot}$ TBox and has the
following two properties (we call a role name $r$ _simple relative to
$\mathcal{T}$_ if there does not exist a role $s$ with $\mathcal{T}\models{\sf
trans}(s)$ and $\mathcal{T}\models s\sqsubseteq r$):

  * •

every model of $\mathcal{T}^{\prime}$ can be extended to a model of
$\mathcal{T}^{\prime\prime}$ by appropriately interpreting the fresh concept
names of $\mathcal{T}^{\prime\prime}$;

  * •

for every model $\mathcal{I}$ of $\mathcal{T}^{\prime\prime}$ there exists a
model $\mathcal{J}$ of $\mathcal{T}^{\prime}$ which coincides with
$\mathcal{I}$ regarding the interpretation of concept names and regarding the
interpretation of role names $r$ that are simple relative to $\mathcal{T}$.
Moreover, for role names $r$ that are not simple relative to $\mathcal{T}$ we
have $r^{\mathcal{J}}\supseteq r^{\mathcal{I}}$.

It follows that $\mathcal{T}^{\prime\prime}$ is as required since role names
that are not simple relative to $\mathcal{T}$ do not occur in any CQs in OMQs.
∎

We require the following standard characterization of FO-definability. Let
$\mathcal{I}$ and $\mathcal{J}$ be interpretations and
$\mathbf{a}=a_{1},\ldots,a_{n}$ a sequence of individual names. Then
$\mathcal{I}$ and $\mathcal{J}$ are called _$m$ -equivalent for $\Sigma$ and
$\mathbf{a}$_, in symbols
$\mathcal{I}\equiv_{m,\Sigma,\mathbf{a}}\mathcal{J}$, if $\mathcal{I}$ and
$\mathcal{J}$ satisfy the same first-order sentences of quantifier rank $\leq
m$ using predicates from $\Sigma$ and individual constants from $\mathbf{a}$
only. The following characterization of FO-definability is well known and can
be proved in a straightforward way.

######  Lemma 18.

Let $Q=(\mathcal{T},\Sigma,q)$ be an OMQ. Then $Q$ is not FO-rewritable iff
for all $m>0$ there are $\Sigma$-ABoxes $\mathcal{A}_{m}$ and
$\mathcal{B}_{m}$ that are consistent with $\mathcal{T}$ and there is
$\mathbf{a}\in\mathsf{Ind}(\mathcal{A}_{m})\cap\mathsf{Ind}(\mathcal{B}_{m})$
such that

  * •

$\mathcal{A}_{m},\mathcal{T}\models q(\mathbf{a})$ and
$\mathcal{B}_{m},\mathcal{T}\not\models q(\mathbf{a})$ and

  * •

$\mathcal{I}_{\mathcal{A}_{m}}\equiv_{m,\Sigma,\mathbf{a}}\mathcal{I}_{\mathcal{B}_{m}}$.

We use Lemma 18 to prove Theorem 4.

See 4

###### Proof.

Let $Q=(\mathcal{T},\Sigma,q)$ be an OMQ in $(\mathcal{L},\text{CQ})$. Assume
$q(\mathbf{x})=\exists\mathbf{y}.\varphi(\mathbf{x},\mathbf{y})$. The
polynomial time algorithm is as follows:

  1. 1.

Let $\mathbf{x}_{1},\ldots,\mathbf{x}_{k}$ and
$\mathbf{y}_{1},\ldots,\mathbf{y}_{k}$ be mutually disjoint subsets of
$\mathbf{x}$ and $\mathbf{y}$, respectively, such that

$\displaystyle\Gamma$ $\displaystyle=$
$\displaystyle\\{q_{1}(\mathbf{x}_{1})=\exists\mathbf{y}_{1}\varphi_{1}(\mathbf{x}_{1},\mathbf{y}_{1}),\ldots,$
$\displaystyle\hskip
8.5359ptq_{k}(\mathbf{x}_{k})=\exists\mathbf{y}_{k}\varphi_{k}(\mathbf{x}_{k},\mathbf{y}_{k})\\}$

is the set of maximal connected subqueries of $q$.

  2. 2.

Obtain $\Gamma^{\prime}$ from $\Gamma$ by removing Boolean CQs $q_{j}$ that
are entailed by the remaining CQs as follows: set $\Gamma_{0}=\Gamma$ and
assume $\Gamma_{0},\ldots,\Gamma_{j}$ have been defined for some $j<k$. Then
set $\Gamma_{j+1}:=\Gamma_{j}\setminus\\{q_{j+1}\\}$ if $q_{j+1}$ is Boolean
and

$\mathcal{A},\mathcal{T}\models\bigwedge_{q_{i}\in\Gamma_{j}\setminus\\{q_{j+1}\\}}q_{i}(\mathbf{a}_{i})\quad\Rightarrow\quad\mathcal{A},\mathcal{T}\models
q_{j}$

holds for all $\Sigma$-ABoxes $\mathcal{A}$ and all $\mathbf{a}_{i}$ in
$\mathsf{Ind}(\mathcal{A})$. Otherwise set $\Gamma_{j+1}:=\Gamma_{j}$. Let
$\Gamma^{\prime}:=\Gamma_{k}$. Clearly, $\Gamma^{\prime}$ can be computed
using an oracle for containment in $(\mathcal{L},\text{CQ})$.

  3. 3.

Check FO-rewritability of $(\mathcal{T},\Sigma,q_{i})$ for all
$q_{i}\in\Gamma^{\prime}$ using an oracle for FO-rewritability in
$(\mathcal{L},\text{conCQ})$.

  4. 4.

Output ‘$Q$ is FO-rewritable’ iff all $q_{i}\in\Gamma^{\prime}$ are FO-
rewritable.

The following claim establishes the correctness of this algorithm.

Claim. $Q$ is FO-rewritable iff all $(\mathcal{T},\Sigma,q_{j})$ with
$q_{j}\in\Gamma^{\prime}$ are FO-rewritable.

The direction from right to left is trivial. Conversely, assume that some
$(\mathcal{T},\Sigma,q_{j})$ with $q_{j}\in\Gamma^{\prime}$ is not FO-
rewritable. By Lemma 18 we find, for all $m>0$, $\Sigma$-ABoxes
$\mathcal{A}_{m}$ and $\mathcal{B}_{m}$ that are consistent relative to
$\mathcal{T}$ and
$\mathbf{a}_{j}\in\mathsf{Ind}(\mathcal{A}_{m})\cap\mathsf{Ind}(\mathcal{B}_{m})$
of the same length as $\mathbf{x}_{j}$ such that

  * •

$\mathcal{A}_{m},\mathcal{T}\models q_{j}(\mathbf{a}_{j})$ and
$\mathcal{B}_{m},\mathcal{T}\not\models q_{j}(\mathbf{a}_{j})$;

  * •

$\mathcal{I}_{\mathcal{A}_{m}}\equiv_{m,\Sigma,\mathbf{a}_{j}}\mathcal{I}_{\mathcal{B}_{m}}$.

Consider the query

$q^{\prime}(\mathbf{x}^{\prime})=\bigwedge_{q_{i}(\mathbf{x}_{i})\in\Gamma^{\prime}\setminus\\{q_{j}(\mathbf{x}_{j})\\}}q_{i}(\mathbf{x}_{i}).$

Observe that $q(\mathbf{x})=q(\mathbf{x}^{\prime},\mathbf{x}_{j})$ and that
$q(\mathbf{x})$ is equivalent to $q_{j}(\mathbf{x}_{j})\wedge
q^{\prime}(\mathbf{x}^{\prime})$. We distinguish two cases.

(1) If $q_{j}$ is not Boolean, then take some $\Sigma$-ABox $\mathcal{A}$ that
is consistent relative to $\mathcal{T}$ and with
$\mathsf{Ind}(\mathcal{A})\cap\mathsf{Ind}(\mathcal{A}_{m})=\emptyset$ and
$\mathsf{Ind}(\mathcal{A})\cap\mathsf{Ind}(\mathcal{B}_{m})=\emptyset$ for all
$m>0$ such that $\mathcal{A},\mathcal{T}\models
q^{\prime}(\mathbf{a}^{\prime})$ for some $\mathbf{a}^{\prime}$ in
$\mathsf{Ind}(\mathcal{A})$ of the same length as $\mathbf{x}^{\prime}$. We
obtain for all $m>0$:

  * •

$\mathcal{A}_{n}\cup\mathcal{A},\mathcal{T}\models
q(\mathbf{a}^{\prime},\mathbf{a}_{j})$ and
$\mathcal{B}_{n}\cup\mathcal{A}\not\models
q(\mathbf{a}^{\prime},\mathbf{a}_{j})$;

  * •

$\mathcal{I}_{\mathcal{A}_{n}\cup\mathcal{A}}\equiv_{n,\Sigma,\mathbf{a}^{\prime},\mathbf{a}_{j}}\mathcal{I}_{\mathcal{B}_{n}\cup\mathcal{A}}$.

It follows from Lemma 18 that $(\mathcal{T},\Sigma,q)$ is not FO-rewritable.

(2) If $q_{j}$ is Boolean, then take some $\Sigma$-ABox $\mathcal{A}$ with
$\mathsf{Ind}(\mathcal{A})\cap\mathsf{Ind}(\mathcal{A}_{m})=\emptyset$ for all
$m>0$ such that $\mathcal{A},\mathcal{T}\models
q^{\prime}(\mathbf{a}^{\prime})$ and $\mathcal{A},\mathcal{T}\not\not\models
q_{j}$ for some $\mathbf{a}^{\prime}$ in $\mathsf{Ind}(\mathcal{A})$ of the
same length as $\mathbf{x}^{\prime}$ (which, since $q_{j}$ is Boolean,
coincides with the length of $\mathbf{x}$). We obtain for all $m>0$:

  * •

$\mathcal{A}_{m}\cup\mathcal{A},\mathcal{T}\models q(\mathbf{a}^{\prime})$ and
$\mathcal{B}_{m}\cup\mathcal{A}\not\models q(\mathbf{a}^{\prime})$;

  * •

$\mathcal{I}_{\mathcal{A}_{m}\cup\mathcal{A}}\equiv_{m,\Sigma,\mathbf{a}^{\prime}}\mathcal{I}_{\mathcal{B}_{m}\cup\mathcal{A}}$.

It follows again from Lemma 18 that $(\mathcal{T},\Sigma,q)$ is not FO-
rewritable. ∎

##  Appendix B Proofs for Section 4

###  B.1 Preliminary: Role intersections

We extend the DLs $\mathcal{E\kern-1.00006ptLIHF}\kern-1.99997pt_{\bot}$ and
$\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot}$ with intersections of
roles that can occur in existential restrictions on the left hand side of
concept inclusions. This extension enables us to reduce entailment of tree-
shaped CQs to TBox reasoning.

An _$\mathcal{ELI}^{\cap}$ concept_ is an $\mathcal{ELI}$ concept that
additionally admits _role intersections_ $R=r_{1}\cap\cdots\cap r_{n}$ of
roles $r_{1},\ldots,r_{n}$ in existential restrictions. We denote role
intersections by $R,S,R^{\prime}$ etc. An _$\mathcal{EL}^{\cap}$ concept_ is
an $\mathcal{EL}$ concept that additionally admits intersections of role names
in existential restrictions. An
_$\mathcal{ELIHF}^{\cap\text{-}\mathsf{lhs}}_{\bot}$ TBox_ is an
$\mathcal{E\kern-1.00006ptLIHF}\kern-1.99997pt_{\bot}$ TBox in which
$\mathcal{ELI}^{\cap}$ concepts can occur on the left hand side of concept
inclusions. Similarly, an _$\mathcal{ELHF}^{\cap\text{-}\mathsf{lhs}}_{\bot}$
TBox_ is an $\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot}$ TBox in
which $\mathcal{EL}^{\cap}$ concepts can occur on the left hand side of
concept inclusions. The semantics of
$\mathcal{ELIHF}^{\cap\text{-}\mathsf{lhs}}_{\bot}$ TBoxes is defined by
extending the semantics of
$\mathcal{E\kern-1.00006ptLIHF}\kern-1.99997pt_{\bot}$ in a straightforward
manner, where we assume that
$R^{\mathcal{I}}=r_{1}^{\mathcal{I}}\cap\cdots\cap r_{n}^{\mathcal{I}}$ for
any interpretation $\mathcal{I}$ and role inclusion $R=r_{1}\cap\cdots\cap
r_{n}$.

The definition of a normal form for TBoxes and Theorem 3 can be easily
extended from $\mathcal{E\kern-1.00006ptLIHF}\kern-1.99997pt_{\bot}$ to
$\mathcal{ELIHF}^{\cap\text{-}\mathsf{lhs}}_{\bot}$: say that an
$\mathcal{ELIHF}^{\cap\text{-}\mathsf{lhs}}_{\bot}$ TBox $\mathcal{T}$ is in
_normal form_ if its concept inclusions take the form

$\displaystyle A\sqsubseteq\bot\quad A\sqsubseteq\exists
r.B\quad\top\sqsubseteq A\quad B_{1}\sqcap B_{2}\sqsubseteq A\quad\exists
R.B\sqsubseteq A$

with $A,B,B_{1},B_{2}$ concept names, $r$ a role, and $R$ a role intersection.
An analogue of Theorem 3 is formulated and proved in the obvious way. We leave
this to the reader.

###  B.2 Preliminary: Canonical models

We introduce the canonical model $\mathcal{I}_{\mathcal{A},\mathcal{T}}$ of an
ABox $\mathcal{A}$ and TBox $\mathcal{T}$ in
$\mathcal{ELIHF}^{\cap\text{-}\mathsf{lhs}}_{\bot}$. The main properties of
$\mathcal{I}_{\mathcal{T},\mathcal{A}}$ are:

  * •

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

  * •

for every model $\mathcal{I}$ of $\mathcal{T}$ there exists a homomorphism
from $\mathcal{I}_{\mathcal{I},\mathcal{A}}$ to $\mathcal{I}$ that maps each
$a\in{\sf Ind}(\mathcal{A})$ to itself.

$\mathcal{I}_{\mathcal{A},\mathcal{T}}$ is constructed using a standard chase
procedure. We will also introduce a variant of this procedure that constructs,
given $\mathcal{A}$ and $\mathcal{T}$, the _completion_ ABox
$\mathcal{A}^{c}_{\mathcal{T}}$ of $\mathcal{A}$ which contains $\mathcal{A}$
and all assertions $A(a)$ and $r(a,b)$ with $a,b\in{\sf Ind}(\mathcal{A})$
that are entailed by $\mathcal{A}$ and $\mathcal{T}$. In both cases we assume
that $\mathcal{A}$ is consistent with $\mathcal{T}$ and that $\mathcal{T}$ is
in normal form.

We start by defining the canonical model
$\mathcal{I}_{\mathcal{A},\mathcal{T}}$ of $\mathcal{A}$ and $\mathcal{T}$. It
is convenient to use ABox notation when constructing
$\mathcal{I}_{\mathcal{A},\mathcal{T}}$ and so we will construct a (possibly
infinite) ABox $\mathcal{A}^{\text{can}}_{\mathcal{T}}$ and define
$\mathcal{I}_{\mathcal{A},\mathcal{T}}$ as the interpretation corresponding to
$\mathcal{A}^{\text{can}}_{\mathcal{T}}$.

Thus assume that $\mathcal{A}$ and $\mathcal{T}$ are given. The _full
completion sequence of $\mathcal{A}$ w.r.t. $\mathcal{T}$_ is the sequence of
ABoxes $\mathcal{A}_{0},\mathcal{A}_{1},\dots$ defined by setting

$\displaystyle\mathcal{A}_{0}$ $\displaystyle=$ $\displaystyle\mathcal{A}\cup$
$\displaystyle\\{r(a,b)\mid s(a,b)\in\mathcal{A},\mathcal{T}\models
s\sqsubseteq r\\}\cup$ $\displaystyle\\{r(a,b)\mid
s(b,a)\in\mathcal{A},\mathcal{T}\models s^{-}\sqsubseteq r\\}$

and defining $\mathcal{A}_{i+1}$ to be $\mathcal{A}_{i}$ extended as follows
(recall that we abbreviate $r(a,b)$ by $r^{-}(b,a)$ and that $r$ ranges over
roles):

  * (i)

if $\exists R.B\sqsubseteq A\in\mathcal{T}$ for $R=r_{1}\cap\cdots\cap r_{n}$
and $r_{1}(a,b),\ldots,r_{n}(a,b),B(b)\in\mathcal{A}_{i}$, then add $A(a)$ to
$\mathcal{A}_{i}$;

  * (ii)

if $\top\sqsubseteq A\in\mathcal{T}$ and $a\in{\sf Ind}(\mathcal{A}_{i})$,
then add $A(a)$ to $\mathcal{A}_{i}$;

  * (iii)

if $B_{1}\sqcap B_{2}\sqsubseteq A\in\mathcal{T}$ and
$B_{1}(a),B_{2}(a)\in\mathcal{A}_{i}$, then add $A(a)$ to $\mathcal{A}_{i}$;

  * (iv)

if $A\sqsubseteq\exists r.B\in\mathcal{T}$ and ${\sf func}(r)\in\mathcal{T}$
and $A(a)\in\mathcal{A}_{i}$ and there exists $b$ with
$r(a,b)\in\mathcal{A}_{i}$, then add $B(b)$ to $\mathcal{A}_{i}$;

  * (v)

if $A\sqsubseteq\exists r.B\in\mathcal{T}$ and ${\sf
func}(r)\not\in\mathcal{T}$ and $A(a)\in\mathcal{A}_{i}$, then take a fresh
individual $b$ and add $r(a,b)$ and $B(b)$ to $\mathcal{A}_{i}$;

  * (vi)

if $r\sqsubseteq s\in\mathcal{T}$ and $r(a,b)\in\mathcal{A}_{i}$, then add
$s(a,b)$ to $\mathcal{A}_{i}$.

Now let $\mathcal{A}_{\mathcal{T}}^{\text{can}}=\bigcup_{i\geq
0}\mathcal{A}_{i}$ and let $\mathcal{I}_{\mathcal{A},\mathcal{T}}$ be the
interpretation corresponding to $\mathcal{A}_{\mathcal{T}}^{\text{can}}$. It
is straightforward to prove the following properties of
$\mathcal{I}_{\mathcal{A},\mathcal{T}}$.

######  Lemma 19.

Assume $\mathcal{A}$ is consistent with $\mathcal{T}$ and $\mathcal{T}$ is in
normal form. Then

  * •

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

  * •

for every model $\mathcal{I}$ of $\mathcal{T}$ there exists a homomorphism
from $\mathcal{I}_{\mathcal{I},\mathcal{A}}$ to $\mathcal{I}$ that maps each
$a\in{\sf Ind}(\mathcal{A})$ to itself.

The ABox $\mathcal{A}_{\mathcal{T}}^{\text{can}}$ can contain additional
individuals and can even be infinite. For some purposes it is more convenient
to work with the subset $\mathcal{A}_{\mathcal{T}}^{c}$ of
$\mathcal{A}_{\mathcal{T}}^{\text{can}}$ that only contains those assertions
in $\mathcal{A}_{\mathcal{T}}^{\text{can}}$ that use individual names from
$\mathcal{A}$. $\mathcal{A}_{\mathcal{T}}^{c}$ can be constructed using rules
as well. For any individual name $a$ we set

$\mathcal{A}|_{a}=\\{A(a)\mid A(a)\in\mathcal{A}\\}$

Now consider the rules (i) to (iv) from above and replace the rules (v) and
(vi) by the single rule

  * (vii)

if $\mathcal{A}_{i}|_{a},\mathcal{T}\models A(a)$, add $A(a)$ to
$\mathcal{A}_{i}$.

Thus, the _completion sequence of $\mathcal{A}$ w.r.t. $\mathcal{T}$_ is the
sequence of ABoxes $\mathcal{A}_{0},\mathcal{A}_{1},\dots$, where
$\mathcal{A}_{0}$ is as defined above and $\mathcal{A}_{i+1}$ is obtained from
$\mathcal{A}_{i}$ by applying the rules (i) to (iv) and (vii) to
$\mathcal{A}_{i}$. The proof of the following is straightforward.

######  Lemma 20.

For all assertions $A(a)$ and $r(a,b)$ with $a,b\in{\sf Ind}(\mathcal{A})$:

  * •

$\mathcal{A},\mathcal{T}\models A(a)$ iff
$A(a)\in\mathcal{A}^{c}_{\mathcal{T}}$;

  * •

$\mathcal{A},\mathcal{T}\models r(a,b)$ iff $r(a,b)\in\mathcal{A}_{0}$ iff
$r(a,b)\in\mathcal{A}^{c}_{\mathcal{T}}$.

###  B.3 ABox Unraveling and Proof of Proposition 8

We show that if a CQ is entailed by an ABox $\mathcal{A}$ and TBox
$\mathcal{T}$, then it is entailed by an unraveling of $\mathcal{A}$ into a
pseudo tree ABox $\mathcal{A}^{\ast}$ and the TBox $\mathcal{T}$. The
corresponding result has been proved for $\mathcal{ELIF}_{\bot}$ TBoxes in
DBLP:conf/kr/BaaderBLW10 and can be extended to $\mathcal{ELIHF}_{\bot}$
TBoxes in a straightforward manner. To formulate the result, we need a notion
of homomorphisms between ABoxes.

######  Definition 21.

Let $\mathcal{A}$, $\mathcal{B}$ be ABoxes. A mapping
$h:\mathsf{Ind}(\mathcal{A})\rightarrow\mathsf{Ind}(\mathcal{B})$ is a
_homomorphism_ if

  * •

$A(a)\in\mathcal{A}$ implies $A(h(a))\in\mathcal{B}$ for all
$a\in\mathsf{Ind}(\mathcal{A})$;

  * •

$r(a,b)\in\mathcal{A}$ implies $r(h(a),h(b))\in\mathcal{B}$ for all
$a,b\in\mathsf{Ind}(\mathcal{A})$.

The following preservation property of homomorphisms w.r.t. certain answers to
CQs is well known.

######  Lemma 22.

Let $Q=(\mathcal{T},\Sigma,q)$ be an OMQ from
($\mathcal{E\kern-1.00006ptLIHF}\kern-1.99997pt_{\bot}$, CQ), $\mathcal{A}$,
$\mathcal{B}$ ABoxes, and $h$ a homomorphism from $\mathcal{A}$ to
$\mathcal{B}$ such that every role that is functional in $\mathcal{B}$ is
functional in $\mathcal{A}$ as well.

  * •

If $\mathcal{B}$ is consistent with $\mathcal{T}$, then $\mathcal{A}$ is
consistent with $\mathcal{T}$;

  * •

if $\mathcal{A}\models Q(\mathbf{a})$, then $\mathcal{B}\models
Q(h(\mathbf{a}))$ for all $\mathbf{a}\subseteq\mathsf{Ind}(\mathcal{A})$.

######  Proposition 23.

Let $Q=(\mathcal{T},\Sigma,q)$ be an OMQ from
$(\mathcal{E\kern-1.00006ptLIHF}\kern-1.99997pt_{\bot},\text{CQ})$ and let
$\mathcal{A}$ be a $\Sigma$-ABox that is consistent with $\mathcal{T}$ such
that $\mathcal{A}\models Q(\mathbf{a})$. Then there is a pseudo tree
$\Sigma$-ABox $\mathcal{A}^{\ast}$ that is consistent with $\mathcal{T}$, of
width at most $|q|$, of outdegree bounded by $|\mathcal{T}|$ and such that
$\mathbf{a}$ is in the core of $\mathcal{A}^{*}$ and the following conditions
are satisfied:

  1. 1.

$\mathcal{A}^{\ast}\models Q(\mathbf{a})$;

  2. 2.

there is a homomorphism from $\mathcal{A}^{\ast}$ to $\mathcal{A}$ that is the
identity on $\mathbf{a}$;

  3. 3.

if a role $r$ is functional in $\mathcal{A}$, then $r$ is functional in
$\mathcal{A}^{\ast}$.

If $\mathcal{T}$ is an $\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot}$
TBox, then there exists a pseudo ditree ABox $\mathcal{A}^{\ast}$ with these
properties.

See 8

###### Proof.

The direction from right to left is trivial. Now assume that
$Q_{1}\not\subseteq Q_{2}$. Then there exists a $\Sigma$-ABox $\mathcal{A}$
that is consistent with $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ and
$\mathbf{a}$ in ${\sf Ind}(\mathcal{A})$ such that $\mathcal{A}\models
Q_{1}(\mathbf{a})$ and $\mathcal{A}\not\models Q_{2}(\mathbf{a})$. By
Proposition 23 there exists a pseudo tree $\Sigma$-ABox $\mathcal{A}^{\ast}$
that is consistent with $\mathcal{T}_{1}$, of width at most $|q_{1}|$ and of
outdegree bounded by $|\mathcal{T}_{1}|$ such that $\mathbf{a}$ is in the core
of $\mathcal{A}^{*}$ with

  * •

$\mathcal{A}^{\ast}\models Q_{1}(\mathbf{a})$;

  * •

there is a homomorphism from $\mathcal{A}^{\ast}$ to $\mathcal{A}$ that is the
identity on $\mathbf{a}$;

  * •

if a role $r$ is functional in $\mathcal{A}$, then $r$ is functional in
$\mathcal{A}^{\ast}$

It follows from Lemma 22 that $\mathcal{A}^{\ast}$ is consistent with
$\mathcal{T}_{2}$ and that $\mathcal{A}^{\ast}\not\models Q_{2}(\mathbf{a})$,
as required. ∎

###  B.4 Preliminary: Tree-shaped queries

We show how Boolean CQs can be rewritten into a set of tree-shaped CQs and
then encoded into $\mathcal{ELIHF}^{\cap\text{-}\mathsf{lhs}}_{\bot}$ TBoxes
in such a way that their entailment due to matches in tree-shaped parts of the
canonical model is preserved.

For a CQ $q$ we denote by $\mathsf{var}(q)$ the set of variables in $q$. A CQ
$q$ is _weakly tree-shaped_ if the undirected graph with nodes
$\mathsf{var}(q)$ and edges $\\{\\{x,x^{\prime}\\}\mid r(x,x^{\prime})\in
q\\}$ is acyclic and connected. $q$ is called _weakly ditree-shaped_ if the
directed graph with nodes $\mathsf{var}(q)$ and edges
$\\{(x,x^{\prime})\mid(x,x^{\prime})\in q\\}$ is a tree.

Given a weakly tree-shaped query $q$ we denote by $C_{q}$ the corresponding
$\mathcal{ELI}^{\cap}$ concept (the obvious $\mathcal{ELI}^{\cap}$ concept for
which for any interpretation $\mathcal{I}$ and any $d\in\Delta^{\mathcal{I}}$
we have $d\in C^{\mathcal{I}}$ iff $\mathcal{I}\models q(d)$). If $q$ is a
Boolean weakly tree-shaped query, we denote by $C_{q}$ the
$\mathcal{ELI}^{\cap}$ concept corresponding to an arbitarily chosen query
$q^{\prime}$ that results from $q$ by regarding one of its variables as an
answer variable (in what follows it will not matter which variable we choose).
Note that if $q$ is a weakly ditree-shaped CQ then we can assume that $C_{q}$
is an $\mathcal{EL}^{\cap}$ concept.

Call an interpretation $\mathcal{I}$ _weakly tree-shaped_ if the undirected
graph with nodes $\Delta^{\mathcal{I}}$ and edges
$\\{\\{d,d^{\prime}\\}\mid(d,d^{\prime})\in r^{\mathcal{I}}\\}$ is acyclic and
connected. Call $\mathcal{I}$ _weakly ditree-shaped_ if the directed graph
with nodes $\Delta^{\mathcal{I}}$ and edges
$\\{(d,d^{\prime})\mid(d,d^{\prime})\in r^{\mathcal{I}}\\}$ is a tree. Observe
that in the canonical model $\mathcal{I}_{\mathcal{A},\mathcal{T}}$ the
interpretation $\mathcal{I}_{a}$ attached to the individual names $a\in{\sf
Ind}(\mathcal{A})$ are weakly tree-shaped. Moreover, if $\mathcal{T}$ is an
$\mathcal{ELHF}^{\cap\text{-}\mathsf{lhs}}_{\bot}$ TBox, then they are weakly
ditree-shaped. It follows that in the canonical model
$\mathcal{I}_{\mathcal{T},\mathcal{A}}$ of an
$\mathcal{E\kern-1.00006ptLIHF}\kern-1.99997pt_{\bot}$ TBox $\mathcal{T}$ and
pseudo tree ABox $\mathcal{A}$ the only non weakly tree-shaped part is the
core of $\mathcal{A}$. Moreover, if $\mathcal{T}$ is a
$\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot}$ TBox then the only non
weakly ditree-shaped part of $\mathcal{I}_{\mathcal{A},\mathcal{T}}$ is again
the core of $\mathcal{A}$. The following result is straightforward.

######  Lemma 24.

For any Boolean CQ $q$ there are sets ${\sf tree}(q)$ and ${\sf dtree}(q)$ of
$\mathcal{ELI}^{\cap}$-concepts and, respectively,
$\mathcal{EL}^{\cap}$-concepts such that

  1. 1.

$|{\sf tree}(q)|\leq 2^{|q|}$ and for any weakly tree-shaped interpretation
$\mathcal{I}$, $\mathcal{I}\models q$ iff there exists $C\in{\sf tree}(q)$
such that $C^{\mathcal{I}}\not=\emptyset$;

  2. 2.

$|{\sf dtree}(q)|\leq 1$ and for any weakly ditree-shaped interpretation
$\mathcal{I}$, $\mathcal{I}\models q$ iff there exists $C\in{\sf dtree}(q)$
such that $C^{\mathcal{I}}\not=\emptyset$.

We use simple $\mathcal{ELIHF}^{\cap\text{-}\mathsf{lhs}}_{\bot}$ TBoxes to
encode entailment of weakly tree-shaped queries. For any set $\mathcal{Q}$ of
$\mathcal{ELI}^{\cap}$ concepts denote by $\mathcal{T}_{\mathcal{Q}}$ the
$\mathcal{ELIHF}^{\cap\text{-}\mathsf{lhs}}_{\bot}$ TBox that is obtained by
computing the normal form of

$\\{C\sqsubseteq A_{C}\mid C\in\mathcal{Q}\\},$

where the $A_{C}$ are fresh concept names for each $C\in\mathcal{Q}$. A
_match_ of a CQ $q=\exists\mathbf{x}\varphi(\mathbf{x},\mathbf{y})$ in an
interpretation $\mathcal{I}$ is a mapping $\pi$ from the variables
$\mathbf{x}\cup\mathbf{y}$ of $q$ into $\Delta^{\mathcal{I}}$ such that
$\mathcal{I}\models\varphi(\pi(\mathbf{x},\mathbf{y}))$.

######  Lemma 25.

Let $Q=(\mathcal{T},\Sigma,q)$, where $\mathcal{T}$ is an
$\mathcal{E\kern-1.00006ptLIHF}\kern-1.99997pt_{\bot}$ TBox and $q$ is Boolean
CQ. Let $\mathcal{A}$ be a pseudo tree $\Sigma$-ABox and
$\mathcal{T}^{\prime}=\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}$. If $q$ has
a match in $\mathcal{I}_{\mathcal{A},\mathcal{T}}$ whose range does not
intersect with the core of $\mathcal{A}$, then
$\mathcal{A},\mathcal{T}^{\prime}\models\exists xA_{C}(x)$ for some $C\in{\sf
tree}(q)$.

Moreover, if $\mathcal{T}$ is an
$\mathcal{E\kern-1.00006ptLHF}\kern-1.99997pt_{\bot}$ TBox and $\mathcal{A}$ a
pseudo ditree $\Sigma$-ABox, then this still holds if $\mathcal{T}^{\prime}$
is replaced by $\mathcal{T}\cup\mathcal{T}_{{\sf dtree}(q)}$ and ${\sf
tree}(q)$ by ${\sf dtree}(q)$.

###  B.5 Proof of Theorem 9

See 9

###### Proof.

(1) $\Rightarrow$ (2). Assume $\varphi$ is an FO rewriting of
$Q=(\mathcal{T},\Sigma,q)$ but (2) does not hold. Let $\text{qr}(\varphi)$
denote the quantifier rank of $\varphi$. Consider first the case in which $q$
is Boolean and take $k>2^{\text{qr}(\varphi)}$ and a $\Sigma$-ABox
$\mathcal{A}$ that is consistent with $\mathcal{T}$ such that

  * •

$\mathcal{A},\mathcal{T}\models q$;

  * •

$\mathcal{A}|_{\leq k},\mathcal{T}\not\models q$;

  * •

$\mathcal{A}|_{>0},\mathcal{T}\not\models q$.

Let $\mathcal{A}^{\prime}$ be the disjoint union of $\text{qr}(\varphi)$ many
copies of $\mathcal{A}|_{>0}$ and $\mathcal{A}|_{\leq k}$, respectively, and
let $\mathcal{A}^{\prime\prime}$ be the disjoint union of $\mathcal{A}$ and
$\mathcal{A}^{\prime}$. We have

  * •

$\mathcal{A}^{\prime\prime},\mathcal{T}\models q$ and
$\mathcal{A}^{\prime},\mathcal{T}\not\models q$ (since $q$ is connected).

Hence $\mathcal{I}_{\mathcal{A}^{\prime\prime}}\models\varphi$ and
$\mathcal{I}_{\mathcal{A}^{\prime}}\not\models\varphi$. On the other hand, one
can easily prove using Ehrenfeucht-Fraïssé games that

  * •

$\mathcal{I}_{\mathcal{A}^{\prime}}\equiv_{\text{qr}(\varphi),\Sigma,()}\mathcal{I}_{\mathcal{A}^{\prime\prime}}$.

It follows that $\mathcal{I}_{\mathcal{A}^{\prime}}\models\varphi$ and we have
derived a contradiction.

Now assume that $q$ is not Boolean. Take $k>2^{\text{qr}(\varphi)}$ and a
$\Sigma$-ABox $\mathcal{A}$ that is consistent with $\mathcal{T}$ and
$\mathbf{a}$ in the core of $\mathcal{A}$ such that

  * •

$\mathcal{A},\mathcal{T}\models q(\mathbf{a})$;

  * •

$\mathcal{A}|_{\leq k},\mathcal{T}\not\models q(\mathbf{a})$.

Let $\mathcal{A}_{0}$ be the disjoint union of $\text{qr}(\varphi)$ many
copies of $\mathcal{A}$ and $\mathcal{A}|_{\leq k}$, respectively. Now let
$\mathcal{A}^{\prime}$ be the disjoint union $\mathcal{A}_{0}$ and
$\mathcal{A}_{|\leq k}$ and let $\mathcal{A}^{\prime\prime}$ be the disjoint
union of $\mathcal{A}_{0}$ and $\mathcal{A}$. We have

  * •

$\mathcal{A}^{\prime\prime},\mathcal{T}\models q(\mathbf{a})$ and
$\mathcal{A}^{\prime},\mathcal{T}\not\models q(\mathbf{a})$ (since $q$ is
connected).

Hence $\mathcal{I}_{\mathcal{A}^{\prime\prime}}\models\varphi(\mathbf{a})$ and
$\mathcal{I}_{\mathcal{A}^{\prime}}\not\models\varphi(\mathbf{a})$. On the
other hand, one can again easily prove using Ehrenfeucht-Fraïssé games that

  * •

$\mathcal{I}_{\mathcal{A}^{\prime}}\equiv_{\text{qr}(\varphi),\Sigma,\mathbf{a}}\mathcal{I}_{\mathcal{A}^{\prime\prime}}$.

It follows that $\mathcal{I}_{\mathcal{A}^{\prime}}\models\varphi(\mathbf{a})$
and we have derived a contradiction.

(2) $\Rightarrow$ (1). Let $k_{0}$ be such that (2) holds. Consider the set
$\Gamma$ of pairs $(\mathcal{A},\mathbf{c})$ of pseudo tree $\Sigma$-ABoxes
$\mathcal{A}$ of width at most $|q|$, outdegree at most $|\mathcal{T}|$, and
depth at most $k_{0}$ that are with to $\mathcal{T}$ and such that
$\mathbf{c}$ is in the core of $\mathcal{A}$ and
$\mathcal{A},\mathcal{T}\models q(\mathbf{c})$.

Now regard each $(\mathcal{A},\mathbf{c})\in\Gamma$ as a CQ
$q_{\mathcal{A},\mathbf{c}}(\mathbf{x})$, where each individual name in
$\mathcal{A}$ is viewed as a variable, and $\mathbf{c}$ corresponds to the
answer variables $\mathbf{x}$. We will show that

$\varphi(\mathbf{x})=\bigvee_{\mathcal{A},\mathbf{c}\in\Gamma}q_{\mathcal{A},\mathbf{c}}(\mathbf{x})$

is an FO-rewriting of $Q$.

Assume $\mathcal{A}$ is a $\Sigma$ ABox that is consistent with $\mathcal{T}$
and $\mathcal{I}_{\mathcal{A}}\models\varphi(\mathbf{a})$. Then
$\mathcal{I}_{\mathcal{A}}\models q_{\mathcal{B},\mathbf{c}}(\mathbf{a})$ for
some $(\mathcal{B},\mathbf{c})\in\Gamma$ and so there is a homomorphism $h$
from $\mathcal{B}$ to $\mathcal{A}$ mapping $\mathbf{c}$ to $\mathbf{a}$. By
definition of $\Gamma$, it holds that $\mathcal{B},\mathcal{T}\models
q(\mathbf{c})$, and therefore $\mathcal{A},\mathcal{T}\models q(\mathbf{a})$.

Assume that $\mathcal{A}$ is a $\Sigma$ ABox that is consistent with
$\mathcal{T}$ and $\mathcal{A},\mathcal{T}\models q(\mathbf{a})$. By
Proposition 23, there is a pseudo tree $\Sigma$-ABox $\mathcal{A}^{\ast}$ of
width at most $|q|$ and outdegree at most $|\mathcal{T}|$ that is consistent
with $\mathcal{T}$ such that

  * •

$\mathcal{A}^{\ast},\mathcal{T}\models q(\mathbf{a})$;

  * •

There is a homomorphism $h$ from $\mathcal{A}^{\ast}$ to $\mathcal{A}$ that is
the identity on $\mathbf{a}$.

Assume first that $q$ is non Boolean. By (2) we have
$\mathcal{A}^{\ast}|_{\leq k_{0}},\mathcal{T}\models q(\mathbf{a})$. Thus
$(\mathcal{A}^{\ast}|_{\leq k_{0}},\mathbf{a})\in\Gamma$. The homomorphism $h$
(restricted to $\mathcal{A}^{\ast}|_{\leq k_{0}}$) shows that
$\mathcal{I}_{\mathcal{A}}\models\varphi(\mathbf{a})$.

Now assume that $q$ is Boolean. Take a minimal subset $\mathcal{A}^{\prime}$
of $\mathcal{A}^{\ast}$ such that $\mathcal{A}^{\prime},\mathcal{T}\models q$.
$\mathcal{A}^{\prime}$ is a pseudo tree $\Sigma$ ABox with some core
$\mathcal{A}_{0}^{\prime}$. By minimality,
$\mathcal{A}^{\prime}|_{>0},\mathcal{T}\not\models q$. Thus, by (2) and
minimality we have $\mathcal{A}^{\prime}|_{\leq k_{0}}=\mathcal{A}^{\prime}$.
Thus $(\mathcal{A}^{\prime},())\in\Gamma$. The homomorphism $h$ (restricted to
$\mathcal{A}^{\prime}$) shows that $\mathcal{I}_{\mathcal{A}}\models\varphi$.

The proof that for $\mathcal{ELFH}_{\bot}$ TBoxes it is sufficient to consider
pseudo ditree $\Sigma$-ABoxes is similar and uses the fact that in Proposition
23 pseudo tree ABoxes can be replaced by pseudo ditree $\Sigma$-ABoxes. ∎

###  B.6 Proof of Theorem 11

See 11

For the pumping argument, we require some preparation. For an ABox
$\mathcal{A}$ and TBox $\mathcal{T}$ we employ the completion sequence
$\mathcal{A}_{0},\mathcal{A}_{1},\ldots$ of $\mathcal{A}$ w.r.t. $\mathcal{T}$
and the completion $\mathcal{A}^{c}_{\mathcal{T}}$ defined in the section on
canonical models. For an ABox $\mathcal{A}$ and individual $a$, we set

$\mathcal{A}|_{a}=\\{A(a)\mid A(a)\in\mathcal{A},A\in{\sf N_{C}}\\}.$

For a set $\mathcal{X}$ of concepts and an individual $u$, we set
$\mathcal{X}(u)=\\{C(u)\mid C\in\mathcal{X}\\}$. Let $\mathcal{A}$ be a pseudo
tree $\Sigma$-ABox and $u\in\mathsf{Ind}(\mathcal{A}_{j})$ for some tree of
$\mathcal{A}$. Define

${\sf AT}_{\mathcal{A}}^{\vdash}(u):=\\{A\in{\sf N_{C}}\mid
A(u)\in\mathcal{A}^{c}_{\mathcal{T}}\\}$

Let $\mathcal{A}_{u}^{\downarrow}$ denote the subtree of $\mathcal{A}_{j}$
rooted at $u$, and let $\mathcal{A}_{u}^{\uparrow}$ be the ABox obtained from
$\mathcal{A}$ by dropping $\mathcal{A}_{u}^{\downarrow}$ from $\mathcal{A}$
except for $u$ itself. Define the _transfer sequence
$\mathcal{X}_{0},\mathcal{X}_{1},\ldots$ of $(\mathcal{A},u)$ w. r. t.
$\mathcal{T}$_ by induction as follows:

  * •

$\mathcal{X}_{0}={\sf AT}_{\mathcal{A}^{0}}^{\vdash}(u)$, where
$\mathcal{A}^{0}=\mathcal{A}_{u}^{\uparrow}$;

  * •

$\mathcal{X}_{1}={\sf AT}_{\mathcal{A}^{1}}^{\vdash}(u)$, where
$\mathcal{A}^{1}=\mathcal{A}_{u}^{\downarrow}\cup\mathcal{X}_{0}(u)$;

  * •

$\mathcal{X}_{2i+2}={\sf AT}_{\mathcal{A}^{2i+2}}^{\vdash}(u)$, where
$\mathcal{A}^{2i+2}=\mathcal{A}^{2i}\cup\mathcal{X}_{2i+1}(u)$, for $i\geq 0$;

  * •

$\mathcal{X}_{2i+1}={\sf AT}_{\mathcal{A}^{2i+1}}^{\vdash}(u)$, where
$\mathcal{A}^{2i+1}=\mathcal{A}^{2i-1}\cup\mathcal{X}_{2i}(u)$, for $i\geq 1$.

The sequence of ABoxes $\mathcal{A}^{0},\mathcal{A}^{1}\ldots$ defined above
is called the _ABox transfer sequence for $(\mathcal{A},u)$ w. r. t.
$\mathcal{T}$_.

######  Lemma 26.

Let $n=|{\sf sig}(\mathcal{T})|+1$. Then $\mathcal{X}_{n}=\mathcal{X}_{m}$ for
all $m>n$ and
$(\mathcal{A}^{n-1})^{c}_{\mathcal{T}}\cup(\mathcal{A}^{n})^{c}_{\mathcal{T}}=\mathcal{A}_{\mathcal{T}}^{c}$.

###### Proof.

By definition, $\mathcal{X}_{m}\subseteq\mathcal{X}_{m+1}$, for all $m>0$.
Moreover, if $\mathcal{X}_{m+1}=\mathcal{X}_{m}$ for some $m>0$ then, by Lemma
20,

  * •

all $\mathcal{A}^{(m+1)+2i}$, $i\geq 0$, coincide;

  * •

all $\mathcal{A}^{(m+2)+2i}$, $i\geq 0$, coincide.

It follows that $\mathcal{X}_{m^{\prime}}=\mathcal{X}_{m}$ for all
$m^{\prime}>m$. ∎

We say that $(\mathcal{A},a)$ and $(\mathcal{B},b)$ _coincide locally w.r.t.
$\mathcal{T}$_ (in symbols
$(\mathcal{A},a)\sim_{\mathcal{T}}(\mathcal{B},b)$):

  * •

$\\{A\in\mathsf{sig}(\mathcal{T})\mid
A(a)\in\mathcal{A}\\}=\\{B\in\mathsf{sig}(\mathcal{T})\mid
B(b)\in\mathcal{B}\\}$;

  * •

for every role $r$ with ${\sf func}(r)\in\mathcal{T}$: there exists
$a^{\prime}$ with $r(a,a^{\prime})\in\mathcal{A}_{a}^{\uparrow}$ iff there
exists $b^{\prime}$ with $r(b,b^{\prime})\in\mathcal{B}_{b}^{\uparrow}$;

  * •

for every role $r$ with ${\sf func}(r)\in\mathcal{T}$: there exists
$a^{\prime}$ with $r(a,a^{\prime})\in\mathcal{A}_{a}^{\downarrow}$ iff there
exists $b^{\prime}$ with $r(b,b^{\prime})\in\mathcal{B}_{b}^{\downarrow}$;

######  Lemma 27.

Let $\mathcal{A}$ and $\mathcal{B}$ be pseudo tree $\Sigma$ ABoxes with
$a\in{\sf Ind}(\mathsf{trees}(\mathcal{A}))$ and $b\in{\sf
Ind}(\mathsf{trees}(\mathcal{B}))$ such that

  * •

$(\mathcal{A},a)$ and $(\mathcal{B},b)$ coincide locally w.r.t. $\mathcal{T}$;

  * •

the transfer sequence of $(\mathcal{A},a)$ w.r.t. $\mathcal{T}$ coincides with
the transfer sequence of $(\mathcal{B},b)$ w.r.t. $\mathcal{T}$ and is given
by $\mathcal{X}_{0},\ldots$.

Denote by $\mathcal{C}$ the ABox obtained from $\mathcal{A}$ by replacing the
subtree $\mathcal{A}_{a}^{\downarrow}$ by $\mathcal{B}_{b}^{\downarrow}$. Then

  * •

$\mathcal{X}_{0},\ldots$ is also the transfer sequence of $(\mathcal{C},b)$
w.r.t. $\mathcal{T}$.

  * •

Given the ABox transfer sequences $\mathcal{A}^{0},\ldots$ and
$\mathcal{B}^{0},\ldots$ of $(\mathcal{A},a)$ and $(\mathcal{B},b)$ w. r. t.
$\mathcal{T}$ , respectively, the ABox transfer sequence
$\mathcal{C}^{0},\ldots$ of $(\mathcal{C},b)$ w. r. t. $\mathcal{T}$ is given
by setting $\mathcal{C}^{2i}=\mathcal{A}^{2i}$ and
$\mathcal{C}^{2i+1}=\mathcal{B}^{2i+1}$, for $i\geq 0$.

###### Proof.

Straightforward using Lemma 20. ∎

Let $Q=(\mathcal{T},\Sigma,q)$ be an OMQ from
$(\mathcal{ELIHF}_{\bot},\text{conCQ})$ and $k\geq 0$. A pair $\mathcal{A}$,
$\mathbf{a}$ with $\mathcal{A}$ a pseudo tree $\Sigma$-ABox and $\mathbf{a}$ a
tuple in the core of $\mathcal{A}$ is a _$k$ -entailment witness_ for $Q$ if

  1. 1.

$\mathcal{A}$ is consistent with $\mathcal{T}$;

  2. 2.

$\mathcal{A},\mathcal{T}\models q(\mathbf{a})$;

  3. 3.

and

     * •

$q$ is not Boolean and $\mathcal{A}|_{\leq k},\mathcal{T}\not\models
q(\mathbf{a})$ or

     * •

$q$ is Boolean, $\mathcal{A}|_{\leq k},\mathcal{T}\not\models q$ and
$\mathcal{A}|_{>0},\mathcal{T}\not\models q$.

If $q$ is Boolean then we say that $\mathcal{A}$ is a $k$-entailment witness
for $Q$ if $\mathcal{A}$, $()$ is a $k$-entailment witness for $Q$.

The following Lemma implies Part 1 of Theorem 11 for queries that are not
Boolean.

######  Lemma 28.

Let $Q=(\mathcal{T},\Sigma,q)$ be an OMQ from
$(\mathcal{ELIHF}_{\bot},\text{conCQ})$. If $q$ is not Boolean, then $Q$ is
not FO-rewritable iff there exists a $k_{0}$-entailment witness for $Q$ of
outdegree bounded by $|\mathcal{T}|$ for $k_{0}=|q|+2^{3m^{2}}$ where
$m=|\mathcal{T}|$.

###### Proof.

The direction $(\Rightarrow)$ follows from Theorem 9. Conversely, assume that
there is a $k_{0}$-entailment witness $\mathcal{A}$, $\mathbf{a}$ for
$Q=(\mathcal{T},\Sigma,q)$. We show that for every $k>k_{0}$ there exists a
$k$-entailment witness for $Q$. Then non FO-rewritability of $Q$ follows from
Theorem 9.

Assume $\mathcal{A}$, $\mathbf{a}$ is a $k$-entailment witness for $Q$ for
some $k\geq k_{0}$. It is sufficient to construct a pseudo tree $\Sigma$-ABox
$\mathcal{B}$ which, together with $\mathbf{a}$ is a $k^{\prime}$-entailment
witness for $Q$ for some $k^{\prime}>k$. We may assume w. l. o. g. that
$\mathcal{A}$ is minimal in the sense that, for every individual $a$ from the
trees of $\mathcal{A}$ we have $\mathcal{A}^{-a},\mathcal{T}\not\models
q(\mathbf{a})$, where $\mathcal{A}^{-a}$ is obtained from $\mathcal{A}$ by
dropping the subtree rooted at $a$ (including $a$).

Let $w$ be a leaf node in $\mathcal{A}$ of maximal distance from the core of
$\mathcal{A}$ and $\rho$ be the root of the tree $\mathcal{A}_{i}$ of
$\mathcal{A}$ containing $w$. Then the distance of $w$ from $\rho$ is at least
$k+1$. Since by Lemma 26 the number of transfer sequences w. r. t.
$\mathcal{T}$ does not exceed $2^{|\mathcal{T}|^{2}}\\!\\!$, on the path from
$\rho$ to $w$ there must be at least two individuals $u_{1}$ and $u_{2}$ with
distance at least $|q|$ from $\rho$ such that

  * (a)

$(\mathcal{A},u_{1})$ and $(\mathcal{A},u_{2})$ coincide locally w.r.t.
$\mathcal{T}$;

  * (b)

the transfer sequences of $(\mathcal{A},u_{1})$ and $(\mathcal{A},u_{2})$
w.r.t. $\mathcal{T}$ coincide;

  * (c)

the transfer sequences of $(\mathcal{A}^{-w}|,u_{1})$ and
$(\mathcal{A}^{-w}|,u_{2})$ w.r.t. $\mathcal{T}$ coincide.

We may assume that $u_{1}$ is between $\rho$ and $u_{2}$. Let $\mathcal{B}$ be
the ABox obtained from $\mathcal{A}$ by replacing
$\mathcal{A}_{u_{2}}^{\downarrow}$ by $\mathcal{A}_{u_{1}}^{\downarrow}$ in
$\mathcal{A}$. By renaming nodes in $\mathcal{A}_{u_{1}}^{\downarrow}$, we can
assume that the root of the subtree $\mathcal{A}_{u_{1}}^{\downarrow}$ of
$\mathcal{B}$ is denoted by $u_{2}$.

We show that $\mathcal{B}$, $\mathbf{a}$ is a $k+1$-entailment witness for
$\mathcal{T}$, $\Sigma$, and $q$. To this end we show:

  1. 1.

$\mathcal{B}$ is consistent relative to $\mathcal{T}$;

  2. 2.

$\mathcal{B},\mathcal{T}\models q(\mathbf{a})$;

  3. 3.

$\mathcal{B}|_{\leq k+1},\mathcal{T}\not\models q(\mathbf{a})$.

First observe that by (a) $(\mathcal{A},u_{1})$ and $(\mathcal{A},u_{2})$
coincide locally w.r.t. $\mathcal{T}$. Thus, since $\mathcal{A}$ is consistent
relative to $\mathcal{T}$, $\mathcal{I}_{\mathcal{B}}$ satisfies the
functionality constraints of $\mathcal{T}$. Also, it follows from (b) and
Lemma 20 and Lemma 27 that we obtain a canonical model
$\mathcal{I}_{\mathcal{B},\mathcal{T}}$ of $\mathcal{B}$ and $\mathcal{T}$ by
replacing the subtree-interpretation rooted at $u_{2}$ in
$\mathcal{I}_{\mathcal{A},\mathcal{T}}$ with the subtree-interpretation rooted
at $u_{1}$ in $\mathcal{I}_{\mathcal{A},\mathcal{T}}$. Thus, $\mathcal{B}$ is
consistent relative to $\mathcal{T}$.

It follows from $\mathcal{A},\mathcal{T}\models q(\mathbf{a})$, the condition
that $q$ is connected, and the fact that $\mathcal{A}$ coincides with
$\mathcal{B}$ for individuals with distance $\leq|q|$ from the core of
$\mathcal{A}$ that $\mathcal{B},\mathcal{T}\models q(\mathbf{a})$.

It follows from (c), Lemma 20, and Lemma 27 that we obtain a canonical model
$\mathcal{I}_{\mathcal{B}^{-w},\mathcal{T}}$ of $\mathcal{B}^{-w}$ and
$\mathcal{T}$ by replacing the interpretation $\mathcal{I}_{u_{2}}$ rooted at
$u_{2}$ in $\mathcal{I}_{\mathcal{A}^{-w},\mathcal{T}}$ with the
interpretation $\mathcal{I}_{u_{1}}$ rooted at $u_{1}$ in
$\mathcal{I}_{\mathcal{A}^{-w},\mathcal{T}}$.

Now recall that $\mathcal{A}^{-w},\mathcal{T}\not\models q(\mathbf{a})$. It
follows from the condition that $q$ is connected and the fact that
$\mathcal{A}^{-w}$ coincides with $\mathcal{B}^{-w}$ for individuals with
distance $\leq|q|$ from the core of $\mathcal{A}$ that
$\mathcal{B}^{-w},\mathcal{T}\not\models q(\mathbf{a})$.

Clearly $\mathcal{B}^{-w}\supseteq\mathcal{B}|_{\leq k+1}$. Thus,
$\mathcal{B}|_{\leq k+1},\mathcal{T}\not\models q(\mathbf{a})$, as required. ∎

We now consider the case in which $q$ is Boolean. Let $\mathcal{A}$ be a
pseudo tree $\Sigma$-ABox. In contrast to the non Boolean case, $q$ can have
matches in the canonical model $\mathcal{I}_{\mathcal{A},\mathcal{T}}$ that do
not hit the core of $\mathcal{A}$. Thus, to ensure that after pumping
$\mathcal{A}$, no additional matches of $q$ are introduced we have to consider
transfer sequences that are invariant under possible matches of $q$.

Given a CQ $q$, we thus consider the additional TBox $\mathcal{T}_{{\sf
tree}(q)}$ defined above and consider transfer sequence relative to
$\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}$ rather than $\mathcal{T}$ only.
Observe that this has the desired effect as the canonical model
$\mathcal{I}_{\mathcal{A},\mathcal{T}}$ is weakly tree-shaped except for the
individuals in its core.

The following Lemma implies Part 2 of Theorem 11.

######  Lemma 29.

Let $Q=(\mathcal{T},\Sigma,q)$ be an OMQ from
$(\mathcal{ELIHF}_{\bot},\text{conCQ})$ If $q$ is Boolean, then $Q$ is not FO-
rewritable iff there exists a $k_{0}$-entailment witness for $Q$ of outdegree
bounded by $|\mathcal{T}|$ for $k_{0}=|q|+2^{4m^{2}}$ where
$m=|\mathcal{T}|+2^{|q|}$.

###### Proof.

We modify the proof of Lemma 28. The direction $(\Rightarrow)$ follows again
from Theorem 9.

Conversely, assume that there is a $k_{0}$-entailment witness for $Q$. We show
that for every $k>k_{0}$ there exists a $k$-entailment witness for $Q$.

Assume $\mathcal{A}$ is a $k$-entailment witness for $Q$ for some $k\geq
k_{0}$. It is sufficient to construct a pseudo tree $\Sigma$-ABox
$\mathcal{B}$ that is consistent relative to $\mathcal{T}$ and is a
$k^{\prime}$-entailment witness for $Q$ for some $k^{\prime}>k$. We may assume
w. l. o. g. that $\mathcal{A}$ is minimal in the sense that, for every
individual $a$ in any tree of $\mathcal{A}$ we have
$\mathcal{A}^{-a},\mathcal{T}\not\models q$.

Let $w$ be a leaf node in $\mathcal{A}$ of maximal distance from the core of
$\mathcal{A}$ and $\rho$ be the root of its tree. Then the distance of $w$
from $\rho$ is at least $k+1$. Since by Lemma 26 the number of transfer
sequences w.r.t. $\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}$ does not exceed
$2^{(|\mathcal{T}|+|\mathcal{T}_{{\sf tree}(q)}|)^{2}}\\!\\!$, on the path
from $\rho$ to $w$ there must be at least two individuals $u_{1}$ and $u_{2}$
with distance at least $|q|$ from $\rho$ such that

  * (a)

$(\mathcal{A},u_{1})$ and $(\mathcal{A},u_{2})$ coincide locally;

  * (b)

the transfer sequences of $(\mathcal{A},u_{1})$ and $(\mathcal{A},u_{2})$
w.r.t. $\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}$ coincide;

  * (c)

the transfer sequences of $(\mathcal{A}^{-w},u_{1})$ and
$(\mathcal{A}^{-w},u_{2})$ w.r.t. $\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}$
coincide.

  * (d)

the transfer sequences of $(\mathcal{A}|_{>0},u_{1})$ and
$(\mathcal{A}|_{>0},u_{2})$ w.r.t. $\mathcal{T}\cup\mathcal{T}_{{\sf
tree}(q)}$ coincide.

We may assume that $u_{1}$ is between $\rho$ and $u_{2}$. Let $\mathcal{B}$ be
the ABox obtained from $\mathcal{A}$ by replacing
$\mathcal{A}_{u_{2}}^{\downarrow}$ by $\mathcal{A}_{u_{1}}^{\downarrow}$ in
$\mathcal{A}$. By renaming nodes in $\mathcal{A}_{u_{1}}^{\downarrow}$, we can
assume that the root of the subtree $\mathcal{A}_{u_{1}}^{\downarrow}$ of
$\mathcal{B}$ is denoted by $u_{2}$.

We show that

  * •

$\mathcal{B}$ is consistent with $\mathcal{T}$;

  * •

$\mathcal{B},\mathcal{T}\models q$;

  * •

$\mathcal{B}|_{>0},\mathcal{T}\not\models q$;

  * •

$\mathcal{B}|_{\leq k+1},\mathcal{T}\not\models q$.

The argument for (a) is the same as in the proof of Lemma 28 and omitted.

In what follows we apply the observation that for any $\Sigma$-ABox
$\mathcal{A}$ one obtains a canonical model of $\mathcal{A}$ and $\mathcal{T}$
from a canonical model of $\mathcal{A}$ and $\mathcal{T}\cup\mathcal{T}_{{\sf
tree}(q)}$ by taking the reduct to the symbols in $\Sigma\cup\mathcal{T}$. In
fact, every canonical model of $\mathcal{A}$ and $\mathcal{T}$ can be obtained
in this way.

It follows from Lemma 20 and Lemma 27 and conditions (b), (c), and (d),
respectively, that we obtain a canonical model

  * (b’)

$\mathcal{I}_{\mathcal{B},\mathcal{T}\cup\mathcal{T}^{q}}$ of $\mathcal{B}$
and $\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}$ by replacing the subtree
rooted at $u_{2}$ in
$\mathcal{I}_{\mathcal{A},\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}}$ with
the subtree rooted at $u_{1}$ in
$\mathcal{I}_{\mathcal{A},\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}}$;

  * (c’)

$\mathcal{I}_{\mathcal{B}^{-w},\mathcal{T}\cup\mathcal{T}^{q}}$ of
$\mathcal{B}^{-w}$ and $\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}$ by
replacing the subtree rooted at $u_{2}$ in
$\mathcal{I}_{\mathcal{A}^{-w},\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}}$
with the subtree rooted at $u_{1}$ in
$\mathcal{I}_{\mathcal{A}^{-w},\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}}$;

  * (d’)

$\mathcal{I}_{\mathcal{B}|_{>0},\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}}$
of $\mathcal{B}|_{>0}$ and $\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}$ by
replacing the subtree rooted at $u_{2}$ in
$\mathcal{I}_{\mathcal{A}|_{>0},\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}}$
with the subtree rooted at $u_{1}$ in
$\mathcal{I}_{\mathcal{A}|_{>0},\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}}$.

To show that $\mathcal{B},\mathcal{T}\models q$, we distinguish two cases: if
$q$ has a match in $\mathcal{I}_{\mathcal{A},\mathcal{T}}$ that intersects
with the core of $\mathcal{A}$, then $q$ has such a match as well in
$\mathcal{I}_{\mathcal{B},\mathcal{T}}$ since $\mathcal{A}$ coincides with
$\mathcal{B}$ for individuals with distance $\leq|q|$ from the core of
$\mathcal{A}$. If $q$ does not have such match, then
$\mathcal{A},\mathcal{T}\cup\mathcal{T}_{{\sf tree}(q)}\models\exists
x\;A_{C}(x)$ for some $C\in{\sf trees}(q)$. But then
$A_{C}^{\mathcal{I}_{\mathcal{A},\mathcal{T}\cup\mathcal{T}_{{\sf
tree}(q)}}}\not=\emptyset$ and so
$A_{C}^{\mathcal{I}_{\mathcal{B},\mathcal{T}\cup\mathcal{T}_{{\sf
tree}(q)}}}\not=\emptyset$. Thus $\mathcal{B},\mathcal{T}\models q$.

$\mathcal{B}|_{>0},\mathcal{T}\not\models q$ follows from (d’) and the fact
that $\mathcal{A}|_{>0},\mathcal{T}\not\models q$.

To show $\mathcal{B}|_{\leq k+1},\mathcal{T}\not\models q$ it is sufficient to
show that $\mathcal{B}^{-w},\mathcal{T}\not\models q$. But this follows from
(c’) and the fact that $\mathcal{A}^{-w},\mathcal{T}\not\models q$. ∎

It remains to prove the claim of Theorem 11 for $\mathcal{ELHF}_{\bot}$ TBoxes
and Boolean queries. In this case, since one can work with pseudo ditree
$\Sigma$-ABoxes rather than arbitrary pseudo tree $\Sigma$-ABoxes one can
employ the linear size TBox $\mathcal{T}_{{\sf dtree}(q)}$ rather than the
possibly exponential size TBox $\mathcal{T}_{{\sf tree}(q)}$. The remaining
part of the proof is exactly the same as before and so one obtains:

######  Lemma 30.

Let $Q=(\mathcal{T},\Sigma,q)$ be an OMQ from
$(\mathcal{ELHF}_{\bot},\text{conCQ})$. If $q$ is Boolean, then $Q$ is not FO-
rewritable iff there exists a $k_{0}$-entailment witness for $Q$ of outdegree
bounded by $|\mathcal{T}|$ for $k_{0}=|q|+2^{4m^{2}}$ where
$m=|\mathcal{T}|+|q|$.

##  Appendix C Proofs for Section 5

###  C.1 Preliminary: Tree Automata

We introduce two-way alternating parity automata on finite trees (TWAPAs). We
assume w.l.o.g. that all nodes in an $m$-ary tree are from
$\\{1,\dots,m\\}^{*}$. For any set $X$, let $\mathcal{B}^{+}(X)$ denote the
set of all positive Boolean formulas over $X$, i.e., formulas built using
conjunction and disjunction over the elements of $X$ used as propositional
variables, and where the special formulas $\mathsf{true}$ and $\mathsf{false}$
are allowed as well. An _infinite path_ $P$ of a tree $T$ is a prefix-closed
set $P\subseteq T$ such that for every $i\geq 0$, there is a unique $x\in P$
with $|x|=i$.

######  Definition 31 (TWAPA).

A _two-way alternating parity automaton (TWAPA) on finite $m$-ary trees_ is a
tuple $\mathfrak{A}=(S,\Gamma,\delta,s_{0},c)$ where $S$ is a finite set of
_states_ , $\Gamma$ is a finite alphabet,
$\delta:S\times\Gamma\rightarrow\mathcal{B}^{+}(\mathsf{tran}(\mathfrak{A}))$
is the _transition function_ with $\mathsf{tran}(\mathfrak{A})=\\{\langle
i\rangle s,\ [i]s\mid-1\leq i\leq m\text{ and }s\in S\\}$ the set of
_transitions_ of $\mathfrak{A}$, $s_{0}\in S$ is the _initial state_ , and
$c:S\rightarrow\mathbbm{N}$ is the _parity condition_ that assigns to each
state a _priority_.

Intuitively, a transition $\langle i\rangle s$ with $i>0$ means that a copy of
the automaton in state $s$ is sent to the $i$-th successor of the current
node, which is then required to exist. Similarly, $\langle 0\rangle s$ means
that the automaton stays at the current node and switches to state $s$, and
$\langle-1\rangle s$ indicates moving to the predecessor of the current node,
which is then required to exist. Transitions $[i]s$ mean that a copy of the
automaton in state $s$ is sent to the relevant successor if that successor
exists (which is not required).111In our automata constructions, we will
explicitly use only transitions of the form $\langle i\rangle s$. The dual
transitions are needed for closure of TWAPAs under complement.

######  Definition 32 (Run, Acceptance).

A _run_ of a TWAPA $\mathfrak{A}=(S,\Gamma,\delta,s_{0},c)$ on a finite
$\Gamma$-labeled tree $(T,L)$ is a $T\times S$-labeled tree $(T_{r},r)$ such
that the following conditions are satisfied:

  1. 1.

$r(\varepsilon)=(\varepsilon,s_{0})$;

  2. 2.

if $y\in T_{r}$, $r(y)=(x,s)$, and $\delta(s,L(x))=\varphi$, then there is a
(possibly empty) set $S\subseteq\mathsf{tran}(\mathfrak{A})$ such that $S$
(viewed as a propositional valuation) satisfies $\varphi$ as well as the
following conditions:

    1. (a)

if $\langle i\rangle s^{\prime}\in S$, then $x\cdot i$ is defined and there is
a node $y\cdot j\in T_{r}$ such that $r(y\cdot j)=(x\cdot i,s^{\prime})$;

    2. (b)

if $[i]s^{\prime}\in S$ and $x\cdot i$ is defined and in $T$, then there is a
node $y\cdot j\in T_{r}$ such that $r(y\cdot j)=(x\cdot i,s^{\prime})$.

We say that $(T_{r},r)$ is _accepting_ if on all infinite paths
$\varepsilon=y_{1}y_{2}\cdots$ of $T_{r}$, the maximum priority that appears
infinitely often is even. A finite $\Gamma$-labeled tree $(T,L)$ is _accepted_
by $\mathfrak{A}$ if there is an accepting run of $\mathfrak{A}$ on $(T,L)$.
We use $L(\mathfrak{A})$ to denote the set of all finite $\Gamma$-labeled tree
accepted by $\mathfrak{A}$.

It is known (and easy to see) that TWAPAs are closed under complementation and
intersection, and that these constructions involve only a polynomial blowup.
It is also known that their emptiness problem can be solved in time single
exponential in the number of states and polynomial in all other components of
the automaton. In what follows, we shall generally only explicitly analyze the
number of states of a TWAPA, but only implicitly take care that all other
components are of the allowed size for the complexity result that we aim to
obtain.

See 12

###### Proof.

(1.) Consider an OMQ $Q=(\mathcal{T},\Sigma,q(\mathbf{x}))$, where
$\mathbf{x}=x_{1},\ldots,x_{n}$. Take fresh concept names $A_{1},\ldots,A_{n}$
and let $\Sigma^{\prime}=\Sigma\cup\\{A_{1},\ldots,A_{n}\\}$. Denote by
$q^{\prime}(\mathbf{x})$ the result of adding the conjuncts $A_{j}(x_{j})$ to
$q(\mathbf{x})$ for $j\in\\{1,\ldots,n\\}$. One can show that
$Q^{\prime}=(\mathcal{T},\Sigma^{\prime},\exists\mathbf{x}q^{\prime}(\mathbf{x}))$
is FO-rewritable iff $Q$ is FO-rewritable. In fact, if $\varphi(\mathbf{x})$
is an FO-rewriting of $Q$, then obtain $\psi(\mathbf{x})$ from
$\varphi(\mathbf{x})$ by adding the conjuncts $A_{j}(x)$ for
$j\in\\{1,\ldots,n\\}$ to $\varphi(\mathbf{x})$. Then
$\exists\mathbf{x}\psi(\mathbf{x})$ is an FO-rewriting of $Q^{\prime}$.

(2.) Let $Q_{i}=(\mathcal{T}_{i},\Sigma,q_{i}(\mathbf{x}))$ be OMQs for
$i=1,2$. We form the Boolean OMQs $Q_{i}^{\prime}$ in the same way as above.
Then $Q_{1}\subseteq Q_{2}$ iff $Q_{1}^{\prime}\subseteq Q_{2}^{\prime}$, as
required. ∎

###  C.2 Preliminary: Forest Decompositions

Before proving Proposition 13, we carefully analyse query matches in canonical
models of pseudo tree ABoxes. We start with the case where the TBox is
formulated in $\mathcal{ELIHF}_{\bot}$ and afterwards consider
$\mathcal{ELHF}_{\bot}$.

Let $q$ be a connected CQ. We use $\mathsf{id}(q)$ to denote the set of all
queries that can be obtained from $q$ by identifying variables. A _forest
decomposition_ of $q$ is a tuple
$F=(q_{\mathsf{core}},q_{1},x_{1},\ldots,q_{k},x_{k},\mu)$ where
$(q_{\mathsf{core}},q_{1},\ldots,q_{k})$ is a partition of (the atoms of) a
query from $\mathsf{id}(q)$, $x_{1},\dots,x_{k}$ are variables from
$q_{\mathsf{core}}$, and $\mu$ is a mapping from
$\mathsf{Var}(q_{\mathsf{core}})$ to $\mathsf{Ind}_{\mathsf{core}}$ such that
the following conditions are satisfied for $1\leq i,j\leq k$;

  1. 1.

$q_{\mathsf{core}}$ is non-empty;

  2. 2.

$q_{i}$ is weakly tree-shaped with root $x_{i}$;

  3. 3.

$\mathsf{Var}(q_{i})\cap\mathsf{Var}(q_{\mathsf{core}})=\\{x_{i}\\}$;

  4. 4.

$\mathsf{Var}(q_{i})\cap\mathsf{Var}(q_{j})\subseteq\mathsf{Var}(q_{\mathsf{core}})$
if $i\neq j$;

  5. 5.

$q_{i}$ contains no atom $A(x_{i})$;

  6. 6.

$x_{i}$ has a single successor in $q_{i}$.

With $\mathsf{fdec}(q)$, we denote the set of all forest decompositions of
$q$. The following lemma shows how certain matches of $q$ in the canonical
models of pseudo tree ABoxes give rise to forest decompositions of $q$.

######  Lemma 33.

Let $\mathcal{T}$ be an $\mathcal{ELIHF}_{\bot}$ TBox, $\mathcal{A}$ a pseudo
tree ABox, and $q$ a Boolean connected CQ. Then the following are equivalent:

  1. 1.

there is a match $\pi$ of $q$ in $\mathcal{I}_{\mathcal{T},\mathcal{A}}$ such
that at least one individual from the core of $\mathcal{A}$ is in the range of
$\pi$;

  2. 2.

there is a forest decomposition $F=(q_{\mathsf{core}},q_{1},x_{1},\ldots,$
$q_{k},x_{k},\mu)$ of $q$ such that

     * •

$\mu$ is a match for $q_{\mathsf{core}}$ in
$\mathcal{I}_{\mathcal{T},\mathcal{A}}$ whose range consists solely of core
individuals from $\mathcal{A}$;

     * •

for $1\leq i\leq k$, there is a match $\pi_{i}$ for $q_{i}$ in
$\mathcal{I}_{\mathcal{T},\mathcal{A}}$ such that $\pi_{i}(x_{i})=\mu(x_{i})$.

Lemma 33 is a minor variation of similar lemmas proved e.g. in Lutz [2008];
proof details are omitted.

It can be verified that there is a polynomial $p$ such that for every
connected CQ $q$, the number of forest decompositions of $q$ is bounded by
$2^{p(|q|)}$.

Now for the case of $\mathcal{ELHF}_{\bot}$. We say that a CQ $q^{\prime}$ is
obtained from a CQ $q$ _by fork elimination_ if $q^{\prime}$ is obtained from
$q$ by selecting two atoms $r(x,z),s(y,z)$ and identifying the variables $x$
and $y$. We call $q^{\prime}$ a _fork rewriting_ of $q$ if $q^{\prime}$ can be
obtained from $q$ by repeated (but not necessarily exhaustive) fork
elimination. We say that $q^{\prime}$ is a _maximal fork rewriting_ of $q$ if
it is a fork rewriting and no further fork elimination is possible. A
_directed forest decomposition_ is defined like a forest decomposition except
that

  1. 1.

$(q_{\mathsf{core}},q_{1},\ldots,q_{k})$ is a partition of (the atoms of) a
fork rewriting of $q$, instead of a query from $\mathsf{id}(q)$;

  2. 2.

the queries $q_{1},\dots,q_{k}$ are required to be weakly ditree-shaped.

We now establish a strengthened version of Lemma 33 for
$\mathcal{ELHF}_{\bot}$ TBoxes.

######  Lemma 34.

When $\mathcal{T}$ is an $\mathcal{ELHF}_{\bot}$ TBox, then the equivalence in
Lemma 33 is true when forest decompositions are replaced with directed forest
decompositions.

###  C.3 Preliminary: Derivation Trees

We characterize entailment of AQs in terms of derivation trees. Fix an
$\mathcal{ELIHF}^{\cap\text{-}\mathsf{lhs}}_{\bot}$ TBox $\mathcal{T}$ in
normal form and an ABox $\mathcal{A}$. A _derivation tree_ for an assertion
$A_{0}(a_{0})$ in $\mathcal{A}$ with $A_{0}\in{\sf N_{C}}\cup\\{\bot\\}$ is a
finite $\mathsf{Ind}(\mathcal{A})\times({\sf N_{C}}\cup\\{\bot\\})$-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:

     * •

$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$;

     * •

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

     * •

$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}$.

Note that the first item 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’ anonymous parts of the
canonical model. In fact, the derivation of $A$ from $A_{1}\sqcap\dots\sqcap
A_{n}$ by $\mathcal{T}$ can involve the introduction of anonymous elements.

We call a TBox $\mathcal{T}$ _satisfiable_ if it has a model. The main
property of derivation trees is the following.

######  Lemma 35.

  1. 1.

$\mathcal{A},\mathcal{T}\models A(a)$ iff $\mathcal{A}$ is inconsistent with
$\mathcal{T}$ or there is a derivation tree for $A(a)$ in $\mathcal{A}$, for
all assertions $A(a)$ with $A\in{\sf N_{C}}$ and
$a\in\mathsf{Ind}(\mathcal{A})$;

  2. 2.

$\mathcal{A}$ is inconsistent with $\mathcal{T}$ iff $\mathcal{T}$ is
unsatisfiable, there is a derivation tree for $\bot(a)$ in $\mathcal{A}$ for
some $a\in\mathsf{Ind}(\mathcal{A})$, or $\mathcal{A}$ violates a
functionality assertion in $\mathcal{T}$.

The proof is a straightforward extension of an analogous result for
$\mathcal{E\kern-1.00006ptLI}_{\bot}$ in Bienvenu et al. [2013]. Details are
omitted.

###  C.4 Proof of Proposition 13

We next give the main automaton construction underlying our upper complexity
bounds, stated as Proposition 13 in the main paper. For convenience, we repeat
the proposition here.

See 13

We start with proving Point 1 of Proposition 13. Let
$Q=(\mathcal{T},\Sigma,q)$ be an OMQ from
$(\mathcal{ELIHF}_{\bot},\text{BCQ})$. The automaton $\mathfrak{A}_{Q}$ is the
intersection of two automata $\mathfrak{A}_{Q,1}$ and $\mathfrak{A}_{Q,2}$ and
the automaton $\mathfrak{A}_{\mathcal{T}}$ from Point 2 of Proposition 13. All
of them run on $(|\mathcal{T}|\cdot|q|)$-ary
$\Sigma_{\varepsilon}\cup\Sigma_{N}$-labeled trees. The first automaton
$\mathfrak{A}_{Q,1}$ accepts the input tree $(T,L)$ iff it is proper. This
automaton is very simple to construct and its number of states is polynomial
in $|\mathcal{T}|$ and independent of $q$; we omit details. The second
automaton $\mathfrak{A}_{Q,2}$ accepts $(T,L)$ iff $\mathcal{A}_{(T,L)}\models
Q$, provided that $\mathcal{A}_{(T,L)}$ is consistent with $\mathcal{T}$.

Before constructing $\mathfrak{A}_{Q,2}$, we first extend the TBox
$\mathcal{T}$ as follows. Let $q_{1},\dots,q_{\ell}$ be the maximal connected
components of the BCQ $q$ from $Q$. We use $\mathcal{Q}$ to denote the set of
queries that contains

  * •

all queries from $\mathsf{id}(q_{1})\cup\cdots\cup\mathsf{id}(q_{\ell})$ which
are weakly tree-shaped;

  * •

the queries $p_{1},\dots,p_{k}$ from any forest decomposition
$(p_{\mathsf{core}},p_{1},x_{1},\ldots,p_{k},x_{k},\mu)$ in
$\mathsf{fdec}(q_{1})\cup\cdots\cup\mathsf{fdec}(q_{\ell})$.

Each query in $q^{\prime}\in\mathcal{Q}$ can be viewed as an
$\mathcal{E\kern-1.00006ptLI}^{\cap}$-concept $C_{q^{\prime}}$. We add to
$\mathcal{T}$ the inclusion $C_{q^{\prime}}\sqsubseteq A_{q^{\prime}}$ for
each $q^{\prime}\in\mathcal{Q}$, and convert to normal form. Call the
resulting TBox $\mathcal{T}^{+}$. The following lemma will guide the
construction of the automaton $\mathfrak{A}_{Q,2}$.

######  Lemma 36.

Let $\mathcal{A}$ be a pseudo tree ABox that is consistent with $\mathcal{T}$.
Then $\mathcal{A},\mathcal{T}\models q$ iff for all maximal connected
components $q_{j}$ of $q$, one of the following properties is satisfied:

  1. 1.

there is a forest decomposition $F=(q_{\mathsf{core}},q_{1},x_{1},\ldots,$
$q_{k},x_{k},\mu)$ of $q_{j}$ such that

     * •

$\mu$ is a match for $q_{\mathsf{core}}$ in
$\mathcal{I}_{\mathcal{T},\mathcal{A}}$ whose range consists solely of core
individuals from $\mathcal{A}$;

     * •

for $1\leq i\leq k$, there is a match $\pi$ for $q_{i}$ in
$\mathcal{I}_{\mathcal{T},\mathcal{A}}$ such that $\pi(x_{i})=\mu(x_{i})$;

  2. 2.

there is a query $q^{\prime}\in\mathsf{id}(q_{j})$ that is weakly tree-shaped
and an $a\in\mathsf{Ind}(\mathcal{A})$ that is not from the core part of
$\mathcal{A}$ and satisfies $\mathcal{A},\mathcal{T}^{+}\models
A_{q^{\prime}}(a)$;

  3. 3.

there is an $a\in\mathsf{Ind}(\mathcal{A})$ and a set $S$ of concept names
from $\mathcal{T}$ such that $a\in A^{\mathcal{I}_{\mathcal{A},\mathcal{T}}}$
for all $A\in S$ and $\mathcal{A}_{S},\mathcal{T}\models q_{j}$, where
$\mathcal{A}_{S}=\\{A(a)\mid A\in S\\}$.

###### Proof.

(sketch) $\mathcal{A},\mathcal{T}\models q$ is witnessed by a match for every
maximal connected component $q_{j}$ of $q$ into the canonical model
$\mathcal{I}_{\mathcal{A},\mathcal{T}}$ of $\mathcal{A}$ and $\mathcal{T}$. We
distinguish three kinds of such matches: (i) Matches that involve a core
individual of $\mathcal{A}$: As $q_{j}$ is connected, by Lemma 33 we directly
obtain Point 1. (ii) Matches that involve a tree individual $a$ of
$\mathcal{A}$ but no core individual define a weakly tree-shaped query
$q^{\prime}$ that results from identifying variables in $q_{j}$. The root of
$q^{\prime}$ is mapped to $a$, and as $C_{q^{\prime}}\sqsubseteq
A_{q^{\prime}}\in\mathcal{T}^{+}$, it follows that
$\mathcal{A},\mathcal{T}^{+}\models A_{q^{\prime}}(a)$. (iii) Matches that do
not involve any ABox individuals: Consider the ABox individual $a$ that is the
root of the anonymous tree $q_{j}$ is mapped to. As $\mathcal{T}^{+}$ is in
normal form, it is easy to prove using canonical models that there is a set
$S$ of concept names from $\mathcal{T}$ such that $a\in
A^{\mathcal{I}_{\mathcal{A},\mathcal{T}}}$ for all $A\in S$ and
$\mathcal{A}_{S},\mathcal{T}\models q_{j}$. ∎

We use $\mathsf{CN}(\mathcal{T}^{+})$ to denote the set of all concept names
in $\mathcal{T}^{+}$ (and likewise for $\mathsf{CN}(\mathcal{T})$) and
$\mathsf{rol}(\mathcal{T}^{+})$ to denote the set of all role intersections in
$\mathcal{T}^{+}$. Define the TWAPA
$\mathfrak{A}_{Q,2}=(S,\Sigma,\delta,s_{0},c)$ by setting

$\displaystyle S=\;$
$\displaystyle\\{s_{0},s^{j}_{\mathsf{core}},s^{j}_{\mathsf{tree}},s^{j}_{\mathsf{anon}}\mid
1\leq j\leq\ell\\}\;\uplus$
$\displaystyle\\{s_{A,a},\,s_{A},\,s_{A,R,a},\,s_{A,R},\,s_{A,R,\uparrow}\mid$
$\displaystyle\quad a\in\mathsf{Ind}_{\mathsf{core}},\
R\in\mathsf{rol}(\mathcal{T}^{+}),\ A\in\mathsf{CN}(\mathcal{T}^{+})\\}$

and $c(s)=1$ for all $s\in S$ (i. e., exactly the finite runs are accepting).
We introduce the transition function $\delta$ in several steps and provide
some explanation along the way. Start by setting for all
$\rho\in\Sigma_{\varepsilon}$

  * •

$\delta(s_{0},\rho)=\displaystyle\bigwedge_{j=1..\ell}\langle 0\rangle
s^{j}_{\mathsf{core}}\vee\langle 0\rangle s^{j}_{\mathsf{tree}}\vee\langle
0\rangle s^{j}_{\mathsf{anon}}$,

which distinguishes the three cases in Lemma 36, for each connected component
of $q$. Next put for all $\rho\in\Sigma_{\varepsilon}$, $\nu\in\Sigma_{N}$,
and $1\leq j\leq\ell$:

  * •

$\displaystyle\delta(s^{j}_{\mathsf{core}},\rho)=\\!\\!\\!\\!\\!\\!\\!\\!\bigvee_{{(p_{\mathsf{core}},p_{1},x_{1},\ldots,p_{k},x_{k},\mu)\in\mathsf{fdec}(q_{j})}\atop{\text{
with }\mu\text{ a homomorphism from }p_{\mathsf{core}}\text{ to
}\rho}}\;\bigwedge_{i\in 1..k}\langle 0\rangle s_{A_{p_{i}},\mu(x_{i})}$;

  * •

$\displaystyle\delta(s^{j}_{\mathsf{tree}},\rho)=\bigvee_{i\in 1..m}\langle
i\rangle s^{j}_{\mathsf{tree}}$;

  * •

$\displaystyle\delta(s^{j}_{\mathsf{tree}},\nu)=\bigvee_{q^{\prime}\in\mathsf{id}(q_{j})}\langle
0\rangle s_{A_{q^{\prime}(x)}}\vee\bigvee_{i\in 1..m}\langle i\rangle
s^{j}_{\mathsf{tree}}$;

  * •

$\displaystyle\delta(s^{j}_{\mathsf{anon}},\rho)=\bigvee_{a\in\mathsf{Ind}(\rho)}\bigvee_{S\subseteq\mathsf{CN}(\mathcal{T})\atop{\mathcal{A}_{S},\mathcal{T}\models
q_{j}}}\Big{(}\bigwedge_{A\in S}\langle 0\rangle s^{j}_{A,a}\Big{)}\;\vee$
$\displaystyle\bigvee_{i\in 1..m}\langle i\rangle s^{j}_{\mathsf{anon}}$;

  * •

$\displaystyle\delta(s^{j}_{\mathsf{anon}},\nu)=\bigvee_{S\subseteq\mathsf{CN}(\mathcal{T})\atop{\mathcal{A}_{S},\mathcal{T}\models
q_{j}}}\Big{(}\bigwedge_{A\in S}\langle 0\rangle
s^{j}_{A}\Big{)}\vee\bigvee_{i\in 1..m}\langle i\rangle
s^{j}_{\mathsf{anon}}$.

The first line selects a forest decomposition as in Point 1 of Lemma 36; lines
two and three select an ABox individual in a tree component of the pseudo tree
ABox $\mathcal{A}_{(T,L)}$ as in Point 2 of that lemma; and lines four and
five select an individual from $\mathcal{A}_{(T,L)}$ as in Point 3, which can
be either in the core part or in a tree part. It remains to implement the
proof obligations expressed by states of the form $s_{A,a}$ and $s_{A}$. The
former indicates that the concept name $A$ is made true in the canonical model
by the core individual $a$ and the latter that $A$ is made true in the
canonical model by the tree individual that corresponds to the current point
of the input tree. We make sure that these obligations are satisfied by
checking the existence of corresponding derivation trees according to Lemma
35. We start with doing this for the core part of pseudo tree ABoxes. Set for
all $\rho\in\Sigma_{\varepsilon}$ and all $\nu\in\Sigma_{N}$:

  * •

$\delta(s_{A,a},\rho)=\mathsf{true}$ if $A(a)\in\rho$ or
$a\in\mathsf{Ind}(\rho)$ and $\top\sqsubseteq A\in\mathcal{T}^{+}$;

  * •

$\displaystyle\delta(s_{A,a},\rho)=\\\ \hskip
2.13394pt\bigvee_{\mathcal{T}^{+}\models A_{1}\sqcap\dotsb\sqcap
A_{n}\sqsubseteq A}\big{(}\langle 0\rangle
s_{A_{1},a}\wedge\dotsb\wedge\langle 0\rangle s_{A_{n},a}\big{)}\vee\\\ \hskip
13.37277pt\bigvee_{\exists R.B\sqsubseteq
A\in\mathcal{T}^{+}}\Big{(}\bigvee_{R^{\prime}(a,b)\in\rho\text{ with
}\mathcal{T}^{+}\models R^{\prime}\sqsubseteq R}\;\langle 0\rangle
s_{B,b}\vee\\\ \hskip 105.27519pt\bigvee_{i\in 1..m}\langle i\rangle
s_{B,R,a}\Big{)}\vee\\\ \hskip 8.53581pt\bigvee_{B\sqsubseteq\exists
r.A\in\mathcal{T}^{+},\
\mathsf{func}(r)\in\mathcal{T}^{+}}\Big{(}\bigvee_{r(b,a)\in\rho}\;\langle
0\rangle s_{B,b}\vee\\\ \hskip 112.95743pt\bigvee_{i\in 1..m}\langle i\rangle
s_{B,r^{-},a}\Big{)}$
if $a\in\mathsf{Ind}(\rho)$ and $A(a)\notin\rho$;

  * •

$\displaystyle\delta(s_{A,R,a},\nu)=\langle 0\rangle s_{A}$ if $a\in\nu$ and
there is an $R^{\prime}\in\nu$ with $\mathcal{T}^{+}\models
R^{\prime}\sqsubseteq R$.

It should be obvious how the above transitions verify the existence of a
derivation tree. Note that the tree must be finite since runs are required to
be finite. We now deal with proof obligations in the trees of pseudo tree
ABoxes. Set for all $\rho\in\Sigma_{\varepsilon}$ and all $\nu\in\Sigma_{N}$:

  * •

$\displaystyle\delta(s_{A},\nu)=$ true for all $s_{A}\in S$ with $A\in\nu$ or
$\top\sqsubseteq A\in\mathcal{T}^{+}$;

  * •

$\delta(s_{A},\nu)=\displaystyle\\!\bigvee_{\mathcal{T}^{+}\models
A_{1}\sqcap\cdots\sqcap A_{n}\sqsubseteq A}\big{(}\langle 0\rangle
s_{A_{1}}\wedge\cdots\wedge\langle 0\rangle s_{A_{n}}\big{)}\;\vee$
$\displaystyle\bigvee_{\exists R.B\sqsubseteq
A\in\mathcal{T}^{+}}\Big{(}\langle 0\rangle
s_{B,R^{-},\uparrow}\vee\bigvee_{i\in 1..m}\langle i\rangle
s_{B,R}\Big{)}\;\vee$
$\displaystyle\bigvee_{B\sqsubseteq\exists r.A\in\mathcal{T}^{+},\
\mathsf{func}(r)\in\mathcal{T}^{+}}\Big{(}\langle 0\rangle
s_{B,r,\uparrow}\vee\bigvee_{i\in 1..m}\langle i\rangle s_{B,r^{-}}\Big{)}$
for all $A\in\mathsf{CN}(\mathcal{T}^{+})$ with $A\notin\nu$;

  * •

$\delta(s_{A,R,\uparrow},\nu)=\langle-1\rangle s_{A}$ if there is an
$R^{\prime}\in\nu$ with $\mathcal{T}^{+}\models R^{\prime}\sqsubseteq R$ and
$\nu\cap\mathsf{Ind}_{\mathsf{core}}=\emptyset$;

  * •

$\delta(s_{A,R,\uparrow},\nu)=\langle-1\rangle s_{A,a}$ if there is an
$R^{\prime}\in\nu$ with $\mathcal{T}^{+}\models R^{\prime}\sqsubseteq R$ and
$a\in\nu$;

  * •

$\delta(s_{A,R},\nu)=\langle 0\rangle s_{A}$ if there is an $R^{\prime}\in\nu$
with $\mathcal{T}^{+}\models R^{\prime}\sqsubseteq R$.

We define $\delta(s,\alpha)=\mathsf{false}$ for all $s\in
S,\alpha\in\Sigma_{\varepsilon}\cup\Sigma_{N}$ not covered above. Using the
intuitions above and Lemmas 33 and 35, one can prove the following.

######  Lemma 37.

Let $(T,L)$ be a $\Sigma_{\varepsilon}\cup\Sigma_{N}$-labeled tree that is
proper and such that $\mathcal{A}_{(T,L)}$ is consistent with $\mathcal{T}$.
Then $\mathfrak{A}_{Q,2}$ accepts $(T,L)$ iff $\mathcal{A}_{(T,L)}\models Q$.

By construction and Lemma 37, the overall TWAPA $\mathfrak{A}_{Q}$ accepts the
tree language described in Proposition 13 and it remains to analyse its size.

First assume that $\mathcal{T}$ is formulated in $\mathcal{ELIHF}_{\bot}$.
Using the bound on the number of forest decompositions from Section C.2, it
can be verified that the size of the extended TBox $\mathcal{T}^{+}$ is at
most $2^{p(|q|+\mathsf{log}(|\mathcal{T}|))}$ for some polynomial $p$ and thus
the same is true for the number of states of the TWAPA $\mathfrak{A}_{Q,2}$.
Since the number of states of $\mathfrak{A}_{Q,1}$ is polynomial in the size
of $\mathcal{T}$ and independent of $q$ and by the size bounds for
$\mathfrak{A}_{\mathcal{T}}$ given in Point 2 of Proposition 13 (and since
intersection blows up TWAPAs only polynomially), the bound of at most
$2^{p(|q|+\mathsf{log}(|\mathcal{T}|))}$ states also applies to the overall
TWAPA $\mathfrak{A}_{Q}$.

Now for case when $\mathcal{T}$ is formulated in $\mathcal{ELHF}_{\bot}$. By
Lemma 34, we can then replace forest decompositions with directed forest
decompositions in the construction of $\mathfrak{A}_{Q}$. Moreover, Point 2 of
Lemma 36, can be replaced with

  1. 2′.

the maximal fork rewriting $q^{\mathsf{f}}_{j}$ of $q_{j}$ is weakly ditree-
shaped and there is an $a\in\mathsf{Ind}(\mathcal{A})$ that is not from the
core part of $\mathcal{A}$ and satisfies $\mathcal{A},\mathcal{T}^{+}\models
A_{q^{\mathsf{f}}_{j}}(a)$

Consequently, the set $\mathcal{Q}$ used in the construction of
$\mathcal{T}^{+}$ now only needs to contain

  * •

the queries $q^{\mathsf{f}}_{1},\dots,q^{\mathsf{f}}_{\ell}$;

  * •

the queries $p_{1},\dots,p_{k}$ from any directed forest decomposition
$(p_{\mathsf{core}},p_{1},x_{1},\ldots,p_{k},x_{k},\mu)$ in
$\mathsf{fdec}(q_{1})\cup\cdots\cup\mathsf{fdec}(q_{\ell})$.

It is then a consequence of the following lemma that the size of the extended
TBox $\mathcal{T}^{+}$ is now bounded by $p(|q|+|\mathcal{T}|)$ for some
polynomial $p$. The same arguments as before then allow us to carry over that
bound to the number of states in $\mathfrak{A}_{Q}$. The following is a
reformulation of Lemma 4 in Lutz-DL-07. Note that this result crucially relies
on Condition 6 from the definition of forest decompositions.

######  Lemma 38.

Let $q$ be a connected BCQ and let $\mathcal{Q}$ be the set of all queries
that occur as a tree component in a directed forest decomposition of $q$. Then
the cardinality of $\mathcal{Q}$ is polynomial in $q$.

We now sketch the construction of the TWAPA $\mathfrak{A}_{\mathcal{T}}$ from
Point 2 of Proposition 13. We first build a TWAPA $\mathfrak{A}$ which accepts
a proper $\Sigma_{\varepsilon}\cup\Sigma_{N}$-labeled tree $(T,L)$ iff
$\mathcal{A}_{(T,L)}$ is inconsistent with $\mathcal{T}$, and then obtain
$\mathfrak{A}_{\mathcal{T}}$ from $\mathfrak{A}$ by complementing and
intersecting with $\mathfrak{A}_{Q,1}$.

We can assume that $\mathcal{T}$ is satisfiable because in all considered
cases,

  1. 1.

TBox satisfiability is not harder than the reasoning problem (containment or
FO rewritability) that we are interested in;

  2. 2.

the result of containment or FO rewritability is trivial if at least one of
the involved TBoxes is unsatisfiable.

By Lemma 35, we thus have to construct $\mathfrak{A}$ such that it accepts the
input tree $(T,L)$ iff a functionality assertion from $\mathcal{T}$ is
violated by $\mathcal{A}_{T,L}$ or there is a derivation tree for $\bot(a)$
for some $a\in\mathsf{Ind}(\mathcal{A}_{(T,L)})$. The former is
straightforward and the latter can be done in almost exactly the same way as
in the automaton $\mathfrak{A}_{Q,2}$ above. To start, we put the following
transitions for all $\rho\in\Sigma_{\varepsilon}$ and all $\nu\in\Sigma_{N}$,
where $s_{0}$ is the initial state:

  * •

$\delta(s_{0},\rho)=\displaystyle\bigvee_{a\in\mathsf{Ind}(\rho)}\langle
0\rangle s_{\bot,a}\vee\bigvee_{i\in 1..m}\langle i\rangle s_{0}$;

  * •

$\delta(s_{0},\nu)=\displaystyle s_{\bot}\vee\bigvee_{i\in 1..m}\langle
i\rangle s_{0}$.

It thus remains to deal with the proof obligations $s_{\bot,a}$ and
$s_{\bot}$, which is done as in $\mathfrak{A}_{Q,2}$ except that we use the
original TBox $\mathcal{T}$ in place of the extended TBox $\mathcal{T}^{+}$
(and treat $\bot$ like a concept name from $\mathsf{CN}(\mathcal{T})$). This
finishes the construction of the automaton $\mathfrak{A}_{\mathcal{T}}$. The
size of at most $p(|\mathcal{T}|)$ states is easily verified. Note that the
construction is essentially independent of $q$ (except for condition (iv) of
properness) because the transitions of $\mathfrak{A}_{Q,2}$ that refer to
forest decompositions are replaced by the transitions given above.

###  C.5 Deciding Containment

We prove the upper bounds for containment stated in Theorem 5. Actually, they
follow directly from Proposition 13, the fact that $Q_{1}\subseteq Q_{2}$
(where $Q_{i}=(\mathcal{T}_{i},\Sigma,q_{i})$) iff
$L(\mathfrak{A}_{Q_{1}})\cap L(\mathfrak{A}_{\mathcal{T}_{2}})\subseteq
L(\mathfrak{A}_{Q_{2}})$ iff $L(\mathfrak{A}_{Q_{1}})\cap
L(\mathfrak{A}_{\mathcal{T}_{2}})\cap\overline{L(\mathfrak{A}_{Q_{2}})}$ is
empty, the closure of TWAPAs under (polynomial) intersection and complement,
and the complexity of TWAPA emptiness.

###  C.6 Deciding FO rewritability

We prove the upper bounds for FO rewritability stated in Theorems 5 and 6. The
proof is based on the characterization from Points 2 (for
$\mathcal{ELIHF}_{\bot}$) and Point 1 (for $\mathcal{ELHF}_{\bot}$) of Theorem
11 and uses the automata from Proposition 13, in a slightly adapted form.

Let $Q=(\mathcal{T},\Sigma,q)$ be an OMQ from ($\mathcal{ELIHF}_{\bot}$,
conBCQ) and $k_{0}=2^{4(|\mathcal{T}|+2^{|q|})^{2}}$ the bound from Point 2 of
Theorem 11. By that theorem, $Q$ is not FO-rewritable iff there is a pseudo
tree ABox $\mathcal{A}$ of width at most $|q|$ and outdegree at most
$|\mathcal{T}|$ that satisfies the following conditions:

  1. 1.

$\mathcal{A}$ is consistent with $\mathcal{T}$;

  2. 2.

$\mathcal{A}\models Q$;

  3. 3.

$\mathcal{A}|_{>0}\not\models Q$;

  4. 4.

$\mathcal{A}|_{\leq k_{0}}\not\models Q$.

We aim to build a TWAPA $\mathfrak{A}$ that accepts representations of such
ABoxes; it then remains to decide emptiness. To deal with the ‘truncated’
ABoxes $\mathcal{A}|_{\leq k_{0}}$, we need to endow
$\Sigma_{\varepsilon}\cup\Sigma_{N}$-labeled trees with a counting component.
More precisely, we now use
$\Sigma_{\varepsilon}\cup(\Sigma_{N}\times[k_{0}])$-labeled trees, where