First-Order Rewritability of Atomic Queries in Horn Description Logics

1 Introduction

A prominent application of description logic (DL) ontologies is to facilitate access to data. Specifically, the ontology serves to assign a semantics to the relation symbols used in the data; it can also provide additional relation symbols that, although not explicitly occurring in the data, can be used in the query. Several approaches to querying data in the presence of ontologies utilize relational databases systems (RDBMSs), aiming to exploit their mature technology, advanced optimization techniques, and the general infrastructure that those systems offer. One of the most popular such approaches is to rewrite the original query and the DL ontology into an SQL query that is passed to the RDBMS for execution [Calvanese et al., 2007; P´erez-Urbina et al., 2009; Chortaras et al., 2011; Gottlob et al., 2011]. Based on the equivalence of first-order (FO) formulas and SQL queries, we call the rewritten query an FO-rewriting.

The FO-rewriting approach to ontology-based data access comes with its own set of DLs specifically designed for this purpose, the so-called DL-Lite family. To guarantee that an FO-rewriting of queries and ontologies always exists, DLs from this family are significantly restricted in expres-

Frank Wolter

Department of Computer Science University of Liverpool, UK

sive power. Unfortunately, this is not acceptable for all applications, in particular when the ontology is used to model the application domain in a detailed way instead of providing only more abstract, database-style constraints. Given that very expressive DLs of the ALC and SHIQ families do not admit tractable query answering (regarding data complexity), a good compromise between expressive power and computational complexity is provided by so-called Horn DLs such as EL, ELI, and Horn-SHIQ. Already in the basic DLs of this kind, such as EL, and for the simplest kind of queries, known as atomic queries (AQs) or instance queries, FO-rewritings are not guaranteed to always exist. To address this problem, other approaches to utilize RDBMSs and related database technology have been brought forward, including the combined approach [Lutz et al., 2009] and rewritings into datalog [P´erez-Urbina et al., 2009; Eiter et al., 2012].

Depending on the application, however, there can still be good reasons to use the FO-rewriting approach for Horn DLs. First, an important feature of this approach is that it allows the ontology to be added on top of the query interface without any modifications to the underlying database. By contrast, the combined approach involves a data completion step, and thus can only be used if data manipulations are permitted. Second, a rewriting into FO queries rather than datalog programs means that one can exploit the comparatively more advanced optimization techniques available for SQL queries. For both reasons, when FO-rewritings happen to exist for the relevant queries and ontologies, the FO-rewriting approach might be very appropriate.

In this paper, we consider ontologies formulated in the Horn DLs EL, ELI⊥, and Horn-SHI. Notably, EL forms the basis of the OWL EL fragment of the OWL 2 web ontology language and is popular as a basic language for largescale ontologies [Baader et al., 2005]. ELI⊥ can be viewed as the smallest DL that contains as a fragment both EL and the core version of DL-Lite, and Horn-SHI is a generalization of ELI⊥ inspired by the well-known DL Horn-SHIQ, but in contrast to the latter does not admit number restrictions [Hustadt et al., 2007]. As an example for why the rewriting approach fails for these DLs, consider the AQ A(x) and the EL ontology T = {∃r.A ⊑ A}. The query A(x) cannot be rewritten into an FO-query in the presence of T , intuitively because T forces the concept name A to be propagated unboundedly along r-chains in the data and thus the rewritten query would have to express transitive closure of r. Of course, such an isolated example does not rule out the possibility that for some AQs and some EL (or Horn-SHI) ontologies, including those that are used in applications, FOrewritings do exist. For example, A(x) is FO-rewritable relative to the EL ontology T ′ = {A ⊑ ∃r.A}, which has a lot of similarity with the aforementioned ontology T . In fact, T ′ can simply be ignored when answering A(x) without losing any answers. Inspired by these observations, the aim of this paper is to study FO-rewritings of AQs in the presence of ontologies formulated in EL, ELI, ELI⊥, and Horn-SHI.

We primarily study the problem to decide, given an atomic query (AQ) q, an ontology T , and a finite set Σ of symbols that are allowed to be used in the data (ABox), whether q is FO-rewritable relative to T over Σ-ABoxes. Note that the restriction of the data signature is natural in many applications of ontology-based data access, cf. [Baader et al., 2010; Bienvenu et al., 2012b]. We show that this problem is EXPTIME-complete for ontologies formulated in Horn-SHI, where the lower bound applies even to ELI ontologies and when the ABox signature is the full signature (that is, it must contain all concept and role names) rather than being an input. For ontologies formulated in EL, the problem remains EXPTIME-complete when the ABox signature is an input (though the lower bound is more difficult to establish), but is only PSPACE-complete when the ABox signature is full.

Our analysis also yields characterizations of the existence of FO-rewritings in terms of the existence of certain treeshaped ABoxes, which are interesting in their own right. Surprisingly, tree-shaped ABoxes can even be replaced with linear ABoxes (single role chains decorated with concept assertions) when the ontology is formulated in EL and the ABox signature is full. Our proofs also yield a way to effectively construct FO-rewritings when they exist. We use this observation to analyze the size of FO-rewritings, showing that they can always be represented by a union of conjunctive queries (UCQ) of at most triple exponential size, and that this bound is essentially optimal: there are families of AQs and EL ontologies for which FO-rewritings exist, but such that every presentation of the rewritings as a UCQ is necessarily tripleexponential in size.

Some proof details are deferred to the appendix of the long version, http://www.informatik.uni-bremen.de/∼clu/papers/.

2 Preliminaries

Let NC and NR 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-SHI concept inclusion (CI) is of the form L ⊑ R, where L and R are concepts defined by the syntax rules

with A ranging over concept names and r over roles. In DLs, ontologies are formalized as TBoxes. A Horn-SHI TBox T is a finite set of Horn-SHI CIs, transitivity assertions trans(r), and role inclusions (RI) r ⊑ s, with r and s roles. Note that different definitions of Horn-SHI can be found in the literature [Hustadt et al., 2007; Eiter et al., 2008; Kazakov, 2009]. As the original definition from [Hustadt et al., 2007] based on polarity is rather technical, we prefer the above (equivalent) definition.

An ELI⊥ TBox is a finite set of inclusions of the form L ⊑ L′ where L,L′ are constructed by the rule above, but without using disjunction. An ELI⊥ TBox that does not use the ⊥ concept is an ELI TBox, and an ELI TBox that does not use inverse roles is an EL TBox.

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 NI. We sometimes write r-(a, b) instead of r(b, a) and use Ind(A) to denote the set of all individual names used in A.

The semantics of DLs is given in terms of interpretations I = (∆I , ·I ), where ∆I is a non-empty set (the domain) and ·I is the interpretation function, assigning to each A ∈ NC a set AI ⊆ ∆I , to each r ∈ NR a relation rI ⊆ ∆I × ∆I , and to each a ∈ NI an element aI ∈ ∆I such that aI1 ̸= aI2 whenever a1 ̸= a2 (the so-called unique name assumption). The interpretation C I ⊆ ∆I of a concept C in I is defined as usual, see [Baader et al., 2003]. An interpretation I satisfies a CI C ⊑ D if C I ⊆ DI , a transitivity assertion trans(r) if rI is transitive, an RI r ⊑ s if rI ⊆ sI , a concept assertion A(a) if aI ∈ AI , and a role assertion r(a, b) if (aI , bI ) ∈ rI . We say that I is a model of a TBox or an ABox if it satisfies all inclusions and assertions in it. An ABox A is consistent w.r.t. a TBox T if A and T have a common model.

An atomic query (AQ) takes the form A(x), with A a concept name and x a variable. We write A, T |= A(a) if aI ∈ AI for all models I of A and T . If A, T |= A(a) and a ∈ Ind(A), then a is a certain answer to A(x) given A and T . We use certT (A(x), A) to denote the set of all certain answers to A(x) given A and T . A first-order query (FOQ), is a first-order formula ϕ 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. As usual, we write ϕ(⃗x) to indicate that the free variables of ϕ are among ⃗x and call ⃗x the answer variables of ϕ. The number of answer variables is the arity of ϕ and a FOQ ϕ is Boolean if it has arity zero. We use ans(I, ϕ) to denote the set of all answers to the FOQ ϕ in the interpretation I; that is, if ϕ is n-ary, then ans(I, ϕ) contains all tuples ⃗ d ∈ (∆I )n such that the FO-sentence ϕ[⃗ d] is satisfied in I (written I |= ϕ[⃗ d]). To bridge the gap between certain answers and "normal" answers, we sometimes view an ABox A as an interpretation IA, defined in the obvious way; see [Lutz and Wolter, 2012].

A signature is a set of concept and role names, which are uniformly called symbols in this context. We use sig(T ) to denote the set of symbols used in the TBox T . A Σ-ABox is an ABox that uses only concept and role names from Σ. We speak of an ABox signature if the purpose of the signature is to fix the symbols permitted in ABoxes.

Definition 1 (FO-rewriting). Let T be a TBox and Σ an ABox signature. A FOQ ϕ(x) is an FO-rewriting of an AQ A(x) relative to T and Σ if certT (A(x),A) = ans(IA, ϕ)

for all Σ-ABoxes A. If there is such a ϕ(x), then A(x) is FO-rewritable relative to T and Σ.

Thus, FO-rewritings reduce the computation of certain answers (which is a form of deduction) to standard query answering on structures (which is a form of model checking).

Example 2. Recall from the introduction that A(x) is not FO-rewritable relative to T = {∃r.A ⊑ A} and the signature Σ = {r,A}. If we add ∃r.⊤ ⊑ A to T , then A(x) is FO-rewritable relative to the resulting TBox and Σ, and ϕ(x) = A(x) ∨ ∃y r(x, y) is an FO-rewriting. If we choose Σ = {A}, then A(x) becomes FO-rewritable also relative to the original T , with the trivial FO-rewriting A(x).

In some applications, the signature of the ABox is not restricted at all and thus, in principle, infinite. However, FOrewritability of an AQ A(x) relative to T and any (potentially infinite) signature Σ ⊆ NC ∪ NR coincides with FOrewritability of A(x) relative to T and the (finite) ABox signature sig(T ) ∩Σ. In fact, any FO-rewriting of A(x) relative to T and Σ is trivially also an FO-rewriting of A(x) relative to T and sig(T ) ∩ Σ, and when ϕ(x) is an FO-rewriting of A(x) relative to T and sig(T ) ∩ Σ, then (i) ϕ(x) is also an FO-rewriting of A(x) relative to T and Σ if A ∈ sig(T ) and (ii) ϕ(x)∨A(x) is an FO-rewriting of A(x) relative to T and Σ otherwise. Consequently, we from now on restrict our attention to ABox signatures Σ with Σ ⊆ sig(T ) and speak of the full signature Σ when Σ = sig(T ).

Atomic queries are closely related to queries of the more general form C(x) with C an EL concept or an ELI concept. Note that such queries can be viewed as tree-shaped conjunctive queries where the root is the only answer variable. The results presented in this paper also capture these more general queries since ϕ(x) is an FO-rewriting of C(x) relative to T and an ABox signature Σ iff it is an FO-rewriting of A(x) relative to T ∪{A ≡ C} and Σ, with A a fresh concept name.

The reasoning problem studied in this paper is as follows: given an AQ A(x), a TBox T , and an ABox signature Σ (with Σ ⊆ sig(T )), decide whether A(x) is FO-rewritable relative to T and Σ and if this is the case, produce an FO-rewriting. We obtain different versions of this problem by varying the language in which the TBox T can be formulated, and by admitting a finite ABox signature Σ as input or fixing it to be the full signature.

We also consider restricted forms of FOQs for rewriting atomic queries, and restricted kinds of ABoxes. A FOQ is a conjunctive query (CQ) if it has the form ∃⃗yϕ(⃗x, ⃗y) with ϕ a conjunction of atoms; it is a union of conjunctive queries (UCQ) if it is a disjunction of CQs. For simplicity, we disallow equality in CQs and UCQs. If an FO-rewriting is a UCQ, we speak of a UCQ-rewriting. With every ABox A, we associate the undirected graph GA with nodes Ind(A) and edges {{a, b} | r(a, b) ∈ A or r(b, a) ∈ A}. An ABox A is acyclic if the corresponding graph GA is acyclic and r(a, b) ∈ A implies that (i) s(a, b) /∈ A for all s ̸= r and (ii) s(b, a) /∈ A for all role names s; A is tree-shaped if it is acyclic and GA is connected. In tree-shaped ABoxes A, we often distinguish one individual ρA ∈ Ind(A) as the root of A.

We often identify a CQ q with the set of its atoms and regard q as an ABox whose individual names are the variables of q. Then q is called acyclic or tree-shaped if the ABox corresponding to q has the same property.

3 FO-rewritability in Horn-SHI and ELI⊥

We show that deciding FO-rewritability in Horn-SHI and ELI⊥ is EXPTIME-complete. To achieve this, we provide a characterization of FO-rewritability in terms of the existence of certain ABoxes, which is of independent interest. We also show how to compute FO-rewritings if they exist and give upper and lower bounds on their size.

We start by observing that it suffices to concentrate on TBoxes that are formulated in ELI⊥ and in normal form, that is, all CIs are of one of the forms

with A, B, B1, B2 concept names and r a role.

Theorem 3. For every Horn-SHI TBox T and ABox signature Σ, one can construct in polynomial time an ELI⊥ TBox T ′ such that for all AQs A(x) with A /∈ sig(T ′ ) \ sig(T ), every FO-rewriting of A(x) relative to T and Σ is an FOrewriting of A(x) relative to T ′ and Σ, and vice versa.

The proof of Theorem 3 is similar to reductions in [Hustadt et al., 2007; Kazakov, 2009]. For the elimination of value restrictions ∀r.B, observe that the CI A ⊑ ∀r.B is logically equivalent to the CI ∃r-.A ⊑ B. In the following, we will generally work with ELI⊥ TBoxes and assume normal form whenever this is more convenient.

The following is a direct consequence of a result by Rossman and the fact that the class of finite pointed structures (IA, a), with A, T |= A(a), is preserved under homomorphisms [Rossman, 2008].

Proposition 4. Let T be an ELI⊥ TBox and Σ an ABox signature. If an AQ A(x) is FO-rewritable relative to T and Σ, then there is a UCQ-rewriting of A(x) relative to T and Σ.

Next, we observe that ABox inconsistency plays a central role for FO-rewritability of AQs relative to ELI⊥ TBoxes.

Example 5. Let T = {∃r.A ⊑ A,A ⊓ B ⊑ ⊥}. Then B(x) is not FO-rewritable since A, T |= B(a) whenever A is inconsistent w.r.t. T , which is the case iff in A, there are individuals a and b such that A(a) ∈ A, a is reachable from b on an r-path, and B(b) ∈ A. Clearly, this condition cannot be expressed by an FO-formula. If we only admit ABoxes that are consistent w.r.t. T , then B(x) is trivially rewritable (it is a rewriting itself).

To make precise the interplay between FO-rewritability of AQs and of ABox inconsistency, we require some further notions. We say that ABox inconsistency is FO-rewritable relative to T and Σ if there is a FOQ ϕ() such that for every Σ-ABox A, A is inconsistent w.r.t. T iff IA |= ϕ(). We call an AQ A(x) FO-rewritable relative to T and consistent ΣABoxes if there exists a FOQ ϕ(x) such that certT (q,A) = ansIA (ϕ) for all Σ-ABoxes A that are consistent w.r.t. T . Finally, we an AQ A(x) is Σ-trivial relative to T if A, T |= A(a) for all Σ-ABoxes A and a ∈ Ind(A). Note that Σ-trivial AQs are FO-rewritable relative to Σ (with x = x a rewriting) and that A(x) is Σ-trivial relative to T iff T |= C ⊑ A for all concept names C ∈ Σ and all C of the form ∃r.⊤ and ∃r-.⊤ with r ∈ Σ. Thus, it is straightforward to check Σ-triviality of AQs.

Proposition 6. Let T be an ELI⊥ TBox, Σ an ABox signature, and A(x) an AQ that is not Σ-trivial relative to T . Then A(x) is FO-rewritable relative to T and Σ iff

1. A(x) is FO-rewritable relative to T and consistent ΣABoxes, and
2. ABox inconsistency is FO-rewritable relative to T , Σ.

Proof. Assume first that Points 1 and 2 hold. Let ϕ1() be an FO-rewriting of ABox inconsistency relative to T and Σ, and let ϕ2(x) be an FO-rewriting of A(x) relative to T and consistent Σ-ABoxes. Then (ϕ1 ∧ x = x) ∨ ϕ2 is an FOrewriting of A(x) relative to T and Σ.

Conversely, assume that there is an FO-rewriting ϕ(x) of A(x) relative to T and Σ, and that A(x) is not Σ-trivial relative to T . Point 1 is trivial since ϕ(x) is an FO-rewriting of A(x) also relative to T and consistent Σ-ABoxes. For Point 2, Proposition 4 implies that we may assume ϕ(x) to be a UCQ q1 ∨ · · · ∨ qn. Let ψ() be the union of all Boolean CQs p such that

• (i) p ⊆ qi (p is a subset of qi) for some 1 ≤ i ≤ n;
• (ii) for all Σ-ABoxes A: if IA |= p, then A is inconsistent w.r.t. T .

We show that ψ() is an FO-rewriting of ABox inconsistency relative to T and Σ. By Point (ii), IA |= ψ() implies that A is inconsistent w.r.t. T . Conversely, assume that A is a ΣABox that is inconsistent w.r.t. T . Since A(x) is not Σ-trivial relative to T , there is a Σ-ABox A0 and a0 ∈ Ind(A0) such that A0, T ̸|= A(a0). Let Ind(A) ∩ Ind(A0) = ∅. We have A0 ∪A, T |= A(a0) since A is inconsistent w.r.t. T . Hence IA∪A0 |= ϕ[a0] and there is a qi such that IA∪A0 |= qi(a0). Let π be a match of qi in IA∪A0 and let p be the Boolean CQ that consists of all atoms in qi whose variables are mapped by π to Ind(A). It is readily checked that p is a disjunct of ψ() and so IA |= ψ(), as required.

Proposition 6 suggests a decomposition of the test for FOrewritability of AQs: first check FO-rewritability of ABox inconsistency and then check FO-rewritability of the AQ relative to consistent ABoxes. In the following, we pursue this approach.

We now develop characterizations of FO-rewritability in terms of the existence of certain ABoxes. For a tree-shaped ABox A with distinguished root ρA and k ≥ 0, we use A|k to denote the restriction of A to all a ∈ Ind(A) with distance from ρA less than or equal to k. Moreover, A\ {ρA} denotes the (acyclic) ABox obtained from A by removing from A all assertions that involve ρA.

Theorem 7. Let T be an ELI⊥ TBox, Σ an ABox signature, and A(x) an AQ.

1. A(x) is FO-rewritable relative to T and consistent ΣABoxes iff there is a k ≥ 0 such that for all tree-shaped Σ-ABoxes A with root ρA that are consistent w.r.t. T : if A, T |= A(ρA), then A|k, T |= A(ρA);
2. ABox inconsistency is FO-rewritable relative to T and Σ iff there is a k ≥ 0 such that for all tree-shaped ΣABox A with root ρA: if A is inconsistent w.r.t. T and A \ {ρA} is consistent w.r.t. T , then A|k is inconsistent w.r.t. T .

Proof (sketch). For the "only if" direction of Point 1, let ϕ be an FO-rewriting of A(x) relative to T and consistent ΣABoxes. By Proposition 4, we may assume ϕ to be a UCQ. Let k be the maximum number of atoms in any CQ in ϕ. It can be shown that k is the required bound, that is, for all treeshaped Σ-ABoxes A with root ρA that are consistent w.r.t. T , A, T |= A(ρA) implies A|k, T |= A(ρA).

For the "if" direction, assume that k satisfies the conditions in Point 1. We consider all minimal tree-shaped Σ-ABoxes A of depth at most k that are consistent w.r.t. T and such that A, T |= A(ρA) andA|k, T ̸|= A(ρA). View each suchABox A as a (tree-shaped) CQ qA in the obvious way with the root ρA translated into the answer variable x, and define ϕ(x) to be the UCQ obtained as the disjunction of all the CQs qA (it is not hard to see that there are only finitely many such queries, up to equivalence). Then ϕ(x) is a UCQ-rewriting of A(x) relative to T and Σ on acyclic Σ-ABoxes. We use a result on 'unraveling tolerance' from [Lutz and Wolter, 2012] to show that such a ϕ(x) must also be a rewriting of A(x) relative to T and Σ (for this argument, it is not sufficient to know that ϕ(x) is a UCQ-rewriting on tree-shaped Σ-ABoxes). The proof of Point 2 is similar.

The following examples illustrate Theorem 7.

Example 8. (1) We use Point 1 of Theorem 7 to show that A(x) is not FO-rewritable relative to T = {∃r.A ⊑ A} and the full ABox signature. In fact, it suffices to observe that the ABoxes Ak = {r(a0, a1), . . . , r(ak, ak+1),A(ak+1)} with ρAk = a0 are consistent w.r.t. T and satisfy Ak, T |= A(ρAk ) and Ak|k, T ̸|= A(ρAk ).

1. In Example 5, it was claimed that ABox inconsistency is not FO-rewritable relative to T = {∃r.A ⊑ A,A ⊓ B ⊑ ⊥} and the full ABox signature. This is a consequence of Point 2 of Theorem 7 and the facts that the ABoxes A′k = Ak ∪{B(a0)} are not consistent w.r.t. T , but with ρA′k = a0, both A′k |k and A′k \ {ρA′k } are consistent w.r.t. T .

(3) In Point 2 of Theorem 7, the precondition that A \ {ρA} has to be consistent w.r.t. T cannot be dropped. To show this, let T = {A ⊑ ⊥}. Then ABox inconsistency is FOrewritable relative to T and Σ = {A, r} (with rewriting ∃xA(x)), but Ak is inconsistent w.r.t. T and Ak|k is consistent w.r.t. T .

To exploit Theorem 7 for developing a decision procedure for FO-rewritability, we prove that the depth and outdegree of the tree-shaped ABoxes considered in that theorem can be bounded. We use |T | to denote the size of the TBox T , that is, the number of symbols needed to write T .

Theorem 9. Let T be an ELI⊥ TBox in normal form, Σ an ABox signature, A(x) an AQ, and n = |T |. Then Points 1 and 2 of Theorem 7 still hold when

1. "there is a k ≥ 0" is replaced with "for k = 23n2" and

1. "tree-shaped Σ-ABox A" is replaced with "tree-shaped Σ-ABox A of outdegree at most n".

Point 1 is established by a very careful pumping argument (here, the presence of inverse roles complicates matters significantly), and Point 2 relies on a selection of the relevant individuals in tree-shaped ABoxes.

Theorem 9 immediately suggests a na¨ıve decision procedure for deciding FO-rewritability: simply enumerate all treeshaped Σ-ABoxes up to the relevant bounds and check that they have the required properties. To obtain better complexity, we construct a tree automaton that accepts precisely those ABoxes which violate the required properties, and use a subsequent emptiness test. Specifically, we work with alternating two-way B¨uchi automata on finite trees, using the two-way feature to handle inverse roles. We obtain EXPTIME upper bounds and establish matching lower bounds via a reduction from subsumption in ELI, which is EXPTIME-hard [Baader et al., 2008]. Theorem 3 lifts the upper bounds to Horn-SHI.

Theorem 10. The following problems are EXPTIMEcomplete, with the lower bounds already applying to ELI (Points 1 and 3) and ELI⊥ (Point 2), and to the full ABox signature:

1. Given a Horn-SHI TBox T , an ABox signature Σ, and an AQ A(x), is A(x) FO-rewritable relative to T and Σ-ABoxes that are consistent w.r.t. T ?
2. Given a Horn-SHI TBox T and an ABox signature Σ, is inconsistency of Σ-ABoxes FO-rewritable relative to T and Σ?
3. Given a Horn-SHI TBox T , an ABox signature Σ, and an AQ A(x), is A(x) FO-rewritable relative to T and Σ?

We now discuss the actual computation of FO-rewritings. A method for computing FO-rewritings of AQs relative to consistent ABoxes and FO-rewritings of ABox inconsistency is implicit in the proof (sketch) of Theorem 7. As explained in the proof of Proposition 6, these rewritings can be combined into FO-rewritings of AQs, without the restriction to consistent ABoxes. By Theorem 3, this can be lifted from ELI⊥ to Horn-SHI. The constructed rewritings are UCQs whose disjuncts are tree-shaped CQs and whose size is at most triple exponential in the size of the TBox. Using constructions from [Lutz and Wolter, 2010; Nikitina and Rudolph, 2012], one can show that this is essentially optimal. The lower bound already applies to ELTBoxes and the full ABox signature.

Theorem 11.

1. For every Horn-SHI TBox T , signature Σ, and AQ A(x) that is rewritable relative to T and Σ, one can effectively construct a UCQ-rewriting ϕ(x) of size at most 222O(|T |2 ) , in time polynomial in the size of ϕ(x).
2. There is a family of EL TBoxes T0, T1, . . . such that for all i ≥ 0, |Ti| ∈ O(i2 ) and A(x) is FO-rewritable relative to Ti and the full ABox signature sig(Ti), but the smallest UCQ-rewriting is of size at least 222i .

4 FO-rewritability in EL

We next consider FO-rewritability relative to TBoxes formulated in the popular lightweight DL EL. Unlike for HornSHI and ELI⊥, we obtain different complexities depending on whether we admit the ABox signature as an input or fix it to be the full signature. Note that, in EL, ABox consistency is not an issue as every ABox is consistent w.r.t. every TBox. The results in this section can be extended to the extension EL⊥ of EL with the ⊥ concept by dealing with inconsistent ABoxes in essentially the same way as was done in Section 3.

Again, we can work with TBoxes in normal form.

Theorem 12. FO-rewritability of AQs relative to EL TBoxes and the full ABox signature can be polynomially reduced to FO-rewritability of AQs relative to EL TBoxes in normal form and the full ABox signature.

Note that Theorem 12 differs from Theorem 3 in that we are interested in FO-rewritability of A(x) relative to the normalized TBox T ′ and the full signature sig(T ′ ), rather than the original signature sig(T ) as in Theorem 3. In fact, proving Theorem 12 requires a more careful construction.

We now show the surprising result that, when the TBox is formulated in EL and the ABox signature is full, the treeshaped ABoxes from Theorem 9 can be replaced with linear ones. Formally, an ABox A is linear if it consists of role assertions r0(a0, a1), . . . , rn-1(an-1, an) with ai ̸= aj for i ̸= j and concept assertions A(a) with a ∈ {a0, . . . , an}.

Theorem 13. Let T be an EL TBox in normal form, A(x) an AQ, n = |T |, and k = 23n2 . Then A(x) is FO-rewritable relative to T and the full ABox signature iff for all linear ABoxes Awith root ρA, A, T |= A(ρA) implies A|k, T |= A(ρA).

Proof. (sketch) In light of Theorem 9, it is sufficient to show that if there is a tree-shaped ABox A with root ρA such that A, T |= A(ρA) and A|k, T ̸|= A(ρA) with k = 23n2 , then there is a linear ABox A′ that satisfies the same properties. Since EL does not allow inverse roles, we can assume w.l.o.g. that A has the shape of a directed tree, that is, whenever r(a, b) ∈ A, then b is further away from the root b than a. Note that the depth of A must exceed k. We can further assume that B(b) ∈ A whenever A|k, T |= B(b), since these assertions can be added without changing the relevant properties of A. By replacing subtrees with the concept assertions that they entail, we can further ensure that there is only a single individual on level k + 1, and no individuals on any level > k + 1. The desired linear ABox A′ is then defined as the restriction of A to assertions that involve only the individuals that appear on the unique path in A of length k + 1. Since A′ |k ⊆ A|k, we have A′ |k, T ̸|= A(ρA). Since all assertions entailed by A|k and T appear in A and all individuals in A \ A′ are on level at most k, we have A′ , T |= A(ρA). The latter argument relies on A being a directed tree.

The following example shows that, even for EL, it is not possible to replace tree-shaped ABoxes with linear ones if we are interested in signatures other than the full signature.

Example 14. Let

choose Σ = {A1, A2, B1, B2, r}, and take the AQ X(x). The tree-shaped ABox A composed of the assertions

with n as in Theorem 9, is of depth exceeding 23n2 , and we can show that A, T |= X(a0), but A|23n2 , T ̸|=X(a0). However, for all linear Σ-ABoxes A, we have A, T |=X(a0) iff A|1, T |= X(a0): since X,X1,X2 /∈ Σ, we can only have A, T |= X(a0) if there is an r-successor b of a0 in A where Z is entailed, or where Y1 and Y2 are entailed. Since Y1, Y2,Z /∈ Σ, this in turn can only be the case when B1(b),B2(b) ∈ A. But then, A|1, T |=X(a0).

Theorem 13 allows us to replace the alternating tree automata in the proof of Theorem 10 with alternating word automata, improving the upper bound to PSPACE.

Theorem 15. Deciding FO-rewritability of an AQ relative to an EL TBox and the full ABox signature is in PSPACE.

We establish matching lower bounds.

Theorem 16. Deciding FO-rewritability of an AQ relative to an EL TBox and an ABox signature Σ is (1) PSPACE-hard when Σ is full and (2) EXPTIME-hard when Σ is an input.

Point 1 is proved by a reduction from the word problem for polynomially space-bounded deterministic Turing machines. For Point 2, we use polynomially space-bounded alternating Turing machines. As both reductions are lengthy and somewhat subtle, we present instead a proof of CONP-hardness, which illustrates some general ideas that are also used in the other reductions.

We reduce propositional tautology to FO-rewritability of AQs relative to EL TBoxes and the full signature. Let ϑ be a propositional formula in negation normal form with variables p1, . . . , pn, and let sub(ϑ) be the set of subformulas of ϑ. Define a TBox T with the CIs:

Lemma 17. ϑ is a tautology iff L0(x) is FO-rewritable relative to T and the full signature.

Proof. First assume that ϑ is not a tautology. Then there is a truth assignment t such that t ̸|= ϑ. Let k = 23|T |2 and define a linear ABox A as the union of

Starting from the assertion L0(a), one can derive Ln(ak,n), then Ln-1(ak,n-1), and so on, until one obtains L0(a1,0).

Note that the generation of L0(a1,0) cannot be 'shortcut' using the inclusion Aϑ ⊑ L0: since t ̸|= ϑ, Aϑ is not derived anywhere on the chain. We thus have A, T |= L0(a1,0), but A|k, T ̸|= L0(a1,0). By Theorem 13, L0 is not FO-rewritable relative to T and the full ABox signature.

Now assume that ϑ is a tautology and that A, T |= L0(a0) with A linear and r(a0, a1), . . . , r(am-1, am) the role assertions in A. Assume to the contrary of what is to be shown that A|k, T ̸|= L0(a0), with k as above. Then m > k. By analyzing T , it can be verified that we must have assertions Vi,i(ai) ∈ A with V ∈ {T, F}, for 1 ≤ i ≤ n. These assertions represent a truth assignment t. Since ϑ is valid, we have t |= ϑ. Again analyzing T , this can be used to show that A|k, T |= L0(a0), a contradiction.

5 RelatedWork

As observed in [Lutz and Wolter, 2011], there is a close connection between FO-rewritability of AQs relative to DL TBoxes and the boundedness problem for datalog programs. In fact, the known 2EXPTIME upper bound for predicate boundedness of connected monadic datalog programs [Cosmadakis et al., 1988] can be used to obtain a 3EXPTIME upper bound for FO-rewritability of an AQ relative to an ELI TBox; via our Proposition 6, this can be extended to ELI⊥ TBoxes. Boundedness was studied also in the context of the µ-calculus, for which it is EXPTIME-complete [Otto, 1999], and for monadic second order logic [Blumensath et al., 2009]. A different approach to FO-rewritability is suggested in [Bienvenu et al., 2013], based on a connection between query answering in DLs and constraint satisfaction problems (CSPs). This approach is different in spirit from ours and tailored towards expressive DLs of the ALC family. However, it also yields a NEXPTIME upper bound for FO-rewritability relative to Horn-SHI TBoxes. Finally, it is shown in [Bienvenu et al., 2012a] that FO-rewritability of AQs relative to a restricted form of EL TBoxes called classical TBoxes is PTIME-complete; that work also analyzes acyclic TBoxes, for which FO-rewritings always exist.

6 FutureWork

It would be interesting to generalize our approach both regarding the query language and the ontology language covered. Regarding the latter, it would be particularly interesting to generalize our results from Horn-SHI to Horn-SHIQ, which we conjecture to be possible using slight extensions of the techniques introduced in this paper. Regarding the query language, it would be interesting to analyze FO-rewriting of conjunctive queries. We believe that a mix of techniques from this paper and those in [Bienvenu et al., 2012b] might provide a good starting point. Finally, existing ontologies should be investigated regarding FO-rewritability. Important questions are: How many atomic queries are FO-rewritable w.r.t. natural ABox signatures? How difficult is it to find FO-rewritings if they exist, and how large are they? Interesting ontologies to consider are GALEN and non-acyclic versions of NCI.

Acknowledgements. M. Bienvenu was supported by ANR project PAGODA (ANR-12-JS02-007-01). C. Lutz was supported by the DFG SFB/TR 8 'Spatial Cognition'.