Efficient Query Rewriting in the Description Logic EL and Beyond

1 Introduction

Ontology-based data access (OBDA) with Description Logics (DLs) is a very active topic of research, which has resulted in various approaches to implementing OBDA in practice [Poggi et al., 2008; Lutz et al., 2009; P´erez-Urbina et al., 2010; Eiter et al., 2012]. A particularly promising such approach is query rewriting, which enables implementations based on conventional relational database systems (RDBMSs), thus taking advantage of those systems' efficiency and maturity [Poggi et al., 2008; Kontchakov et al., 2013]. The general idea is to transform the original query q and the relevant TBox T into a first-order (FO) query qT that is then handed over to the RDBMS for execution. One limitation of this approach is that, for the majority of description logics that are used as ontology languages, the query qT is not guaranteed to exist. In fact, this is the case already for the members of the popular EL family of lightweight DLs [Baader et al., 2005; Lutz et al., 2009], which underly the EL profile of the OWL2 ontology language and are frequently used in health care and biology ontologies. This observation, however, does not rule out the possibility that FO-rewritings still exist in many practically relevant cases. In fact, TBoxes that emerge from practical applications tend to have a rather simple structure and one might thus speculate that, indeed, FO-rewritings under EL-TBoxes tend to exist in practice.

In this paper, we consider the construction of FO-rewritings of concept queries under TBoxes that are formulated in the description logic ELHdr . The latter is a logical core

Frank Wolter

University of Liverpool, UK frank@csc.liv.ac.uk

of OWL2 EL that extends basic EL with role inclusions and domain/range restrictions on roles [Lutz et al., 2009] while concept queries take the form C(x) with C an EL-concept. Constructing the desired rewritings is computationally hard: it follows from results in [Bienvenu et al., 2013] that deciding whether a given concept query C(x) is FO-rewritable under a given TBox T is PSPACE-complete both in EL and in ELHdr , and it even becomes EXPTIME-complete when the vocabulary of the admitted database instances (i. e., ABoxes) is an additional input-a feature that we allow in the current paper.

Existing approaches to query rewriting under DL TBoxes can be summarized as follows: (i) approaches that target rewritings into the more expressive query language datalog and which are incomplete in the sense that existing datalogrewritings are not guaranteed to be found and, moreover, the generated datalog-rewritings are not necessarily nonrecursive even if there is an FO-rewriting [Rosati, 2007; P´erez-Urbina et al., 2010; Kaminski and Grau, 2013; Mora and Corcho, 2013]; (ii) backwards chaining approaches for existential rules (a strict generalization of ELHdr ) which are complete in the sense that they find an FO-rewriting if there is one, but need not terminate otherwise [K¨onig et al., 2012]; (iii) complete and terminating approaches which aim to prove upper complexity bounds, but which are not practically feasible [Bienvenu et al., 2013; 2014].

The aim of this paper is to design, for the first time, algorithms for computing FO-rewritings of concept queries under EL- and ELHdr -TBoxes that are complete, terminating, and feasible in practice. We start with a marriage of approaches (ii) and (iii) above to get the best of both worlds; in particular, (ii) appears to be practically much more feasible than (iii) while (iii) provides a way to achieve termination. The resulting backwards chaining algorithm is conceptually simple and constitutes a significant step towards our goal. However, it produces FO-rewritings that are unions of conjunctive queries (UCQs), which has two significant drawbacks: first, recent experiments [Lutz et al., 2013] have shown that executing UCQ-rewritings on RDBMSs is prohibitively expensive while executing equivalent rewritings that take the form of non-recursive datalog programs is much more feasible; and second, UCQ-rewritings can be of excessive size even in practically relevant cases [Rosati and Almatelli, 2010].

To address these shortcomings, the main contribution of this paper is to refine our initial backwards chaining algorithm to what we call a decomposed algorithm. While the initial algorithm uses tree-shaped conjunctive queries (CQs) as an internal data structure, the new algorithm only represents single nodes of tree-shaped CQs together with information of how to reassemble these nodes into full queries. This can be seen as a way to implement structure sharing and allows us to directly produce rewritings that are non-recursive datalog programs, avoiding UCQ-rewritings altogether. The algorithm runs in exponential time, is capable of deciding the existence of FOrewritings in EXPTIME (which is optimal), and is capable of producing monadic non-recursive datalog rewritings that are of at most exponential size (but much smaller in practice). We also show that an exponential blowup is unavoidable when rewriting into monadic non-recursive datalog. Technically, the decomposed algorithm is much more subtle than the initial one.

We then evaluate the decomposed algorithm by carrying out experiments with seven ontologies from practical applications. We ask for an FO-rewriting of every concept query A(x) with A a concept name from the ontology under consideration. Out of 10989 inputs in total and with a timeout of 30 seconds, the decomposed algorithm terminates on all but 127 inputs and on average needs less than 0.5 seconds per input. We also analyse the size of the generated non-recursive datalog rewritings, with extremely encouraging results. Our experiments show that the decomposed algorithm performs very well on ontologies from practical applications and also confirm our initial belief that such ontologies very often admit FO-rewritings. In particular, only 74 of 10989 inputs turn out to be not FO-rewritable.

Proof details are deferred to the appendix, available at http://www.informatik.uni-bremen.de/tdki/p.html.

2 Preliminaries

We use NC and NR to denote mutually disjoint countably infinite sets of concept and role names, respectively. An EL-concept is formed according to the syntax rule C ::= A | ⊤ | C ⊓ C | ∃r.C, where A ∈ NC and r ∈ NR. Let C,D be EL-concepts and r, s be role names. Then C ⊑ D is a concept inclusion (CI), r ⊑ s is a role inclusion (RI), dom(r) ⊑ C is a domain restriction, and ran(r) ⊑ C is a range restriction. An ELH-TBox is a finite set of CIs and RIs and an ELHdr -TBox additionally admits domain and range restrictions. The semantics of concepts and TBoxes is defined as usual [Baader et al., 2007; 2005]. For a CI or RI α, we write T |= α if every model of T satisfies α; when T is empty, we write |= α.

An ABox A is a set of assertions of the form A(a) and r(a, b) with A a concept name, r a role name, and a, b individual names from a countably infinite set NI. We use ind(A) to denote the set of individual names that occur in A. A concept query is an expression C(x) with C an EL-concept. We write A, T |= C(a) and say that a is a certain answer to C given the ABox A and TBox T if a ∈ ind(A) and aI ∈ C I for all models I of T and A. A signature is a finite set Σ ⊆ NC∪NR. An ABox is a Σ-ABox if it only uses concept and role names from Σ.

For an FO-formula q(x) with one free variable x, we write A |= q(a) if A (viewed as an interpretation) satisfies q under the assignment that maps x to a. A concept query C(x) is FO-rewritable under a TBox T and signature Σ if there is an FO-formula ϕ(x) such that for all Σ-ABoxes A and individuals a, we have A, T |= C(a) iff A |= ϕ(a). In this case, we call ϕ(x) an FO-rewriting of C(x) under T and Σ. When studying FO-rewritability of concept queries C(x), we can assume w. l. o. g. that C is a concept name since C(x) is FOrewritable under a TBox T and Σ iff A(x) is FO-rewritable under T ∪ {C ⊑ A} and Σ, where A is a fresh concept name [Bienvenu et al., 2013].

We will also consider other forms of rewritings, in particular into unions of conjunctive queries (UCQs) and nonrecursive datalog programs. Although, strictly speaking, non-recursive datalog rewritings are not FO-rewritings, the existence of either kind of rewriting coincides with the existence of an FO-rewriting [Bienvenu et al., 2014]. In particular, non-recursive datalog rewritings can be viewed as a compact representation of a UCQ-rewriting. We will also consider monadic datalog as a special case, where all intensional (IDB) predicates are unary.

For any of these rewritings, if Σ is the set of all concept and role names in T and C, then C(x) is rewritable under T and Σ iff it is rewritable under T and any signature. If this is the case, we say that C(x) is rewritable under T and the full signature.

For our technical constructions, it will be convenient to view EL-concepts as conjunctive queries (CQs) that take the form of a directed tree. We will represent such queries as sets of atoms of the form A(x) and r(x, y) with A a concept name, r a role name and x, y variables. Tree-shapedness of a conjunctive query q then means that the directed graph (V, {(x, y) | r(x, y) ∈ q}) is a tree, where V is the set of variables in q, and that r(x, y), s(x, y) ∈ q implies r = s. We will not distinguish explicitly between an EL-concept C and its query representation. We thus use var(C) to denote the set of variables that occur in C and xε to denote the root variable in C. For an x ∈ var(C), we use C|x to denote the EL-concept represented by (the subtree rooted at) x. When we speak of a top-level conjunct (tlc) of an EL-concept C, we mean a concept name A such that A(xε) ∈ C or a concept ∃r.D such that r(xε, y) ∈ C and D = C|y. We use tlc(C) to denote the set of all top-level conjuncts of C. For any syntactic object (such as a concept or a TBox), we define its size to be the number of symbols used to write it.

We show that we can remove domain and range restrictions from ELHdr -TBoxes and work with ELH-TBoxes when developing algorithms that decide rewritability or compute rewritings.

Lemma 1. For every ELHdr -TBox T, signature Σ, and concept query A0(x), one can construct in polynomial time an ELH-TBox T ′ and signature Σ′ such that A0(x) is FOrewritable under T and Σ iff it is FO-rewritable under T ′ and Σ′ .

Moreover, every UCQ and non-recursive datalog rewriting of A0(x) under T ′ and Σ′ can be converted in linear time into a UCQ and, respectively, non-recursive datalog rewriting of A0 under T and Σ.

3 A Backwards Chaining Algorithm

The algorithm presented in this section constructs a set of UCQ-rewritings of A0(x) under an ELH-TBox T by starting from {A0} and then exhaustively applying the axioms in T as rules in a backwards chaining manner. It terminates by either constructing a UCQ-rewriting or returning 'not FOrewritable'. For simplicity and since the purpose of the algorithm presented here is mainly to prepare for the subsequent, more refined one, we consider rewritability for the full signature only.

Let A0 and T be an input to the algorithm. We start with introducing the central backwards chaining steps. Let C and D be EL-concepts and let α be a (concept or role) inclusion from T . The notion of D being obtained from C by applying α is defined as follows.

(CI) Let α = E ⊑ F be a CI, x ∈ var(C), and let there be at least one tlc G of C|x with |= F ⊑ G. Then D is obtained from C by applying α at x if D can be obtained from C by

• removing A(x) for all concept names A with |= F ⊑ A;
• removing the subtree rooted at y whenever r(x, y) ∈ C and |= F ⊑ ∃r.(C|y) (including the edge r(x, y));
• adding A(x) for all concept names A that are a tlc of E;
• adding the subtree ∃r.H to x for each ∃r.H that is a tlc of E.

(RI) Let α = r ⊑ s be an RI and let s(x, y) ∈ C . Then D is obtained from C by applying α at s(x, y) if D can be obtained from C by replacing s(x, y) by r(x, y).

The following is immediate.

Lemma 2. If T |= C ⊑ A0 and D can be obtained from C by applying some inclusion in T , then T |= D ⊑ A0.

Apart from applying backwards chaining, our algorithm also minimises the generated concepts to attain completeness and termination. To make this precise, we introduce some notation. Let C and D be EL-concepts and x ∈ var(C). Then C \ C|x denotes the concept obtained by removing from C the subtree rooted at x, and we write C ≺ D if there exists x ∈ var(D) such that C = D \ D|x. We use ≺∗ to denote the reflexive and transitive closure of ≺ and say that C is ≺- minimal with T |= C ⊑ A0 if T |= C ⊑ A0 and there is no C ′ ≺ C with T |= C ′ ⊑ A0. Note that if T |= C ⊑ A0, then it is possible to find in polynomial time a C ′ ≺∗ C that is ≺-minimal with T |= C ′ ⊑ A0.

The constructions in [Bienvenu et al., 2013] suggest that, to achieve termination, we can use a certain form of blocking, similar to the blocking used in DL tableau algorithms. Let sub(T ) denote the set of subconcepts of (concepts that occur in) T . For each EL-concept C and x ∈ var(C), we set conCT (x) := {D ∈ sub(T ) | T |= C|x ⊑ D}. We say that C is blocked if there are x1, x2, x3 ∈ var(C) such that

1. x1 is a proper ancestor of x2 is an ancestor of x3 and

The algorithm is formulated in Figure 1. Note that, by Lemma 2, the concept D considered in the condition of the while loop satisfies T |= D ⊑ A0 and thus we are guaranteed to find the desired D′ . Also note that each of the potentially many candidates for D′ will work.

procedure find-rewriting(A0(x), T )

return the UCQ ∨M.

Figure 1: The backwards chaining algorithm

Example 3. Let T = { ∃r.(B1 ⊓ B2) ⊑ A0, ∃s.B2 ⊑ B2 }. Starting with M = {A0} and applying the first CI to A0, we get M = {A0, ∃r.(B1 ⊓B2)}. The second CI can be applied repeatedly, starting with ∃r.(B1 ⊓ B2), and yields concepts

all of which are ≺-minimal with T |= Di ⊑ A0. D3 is blocked and the algorithm will classify A0 as 'not FOrewritable' under T .

Now consider the TBox T ′ = T ∪{B1 ⊑ B2}. Already the concept D1 is not ≺-minimal with T ′ |= D1 ⊑ A0 and instead of D1, ∃r.B1 is added toM. At this point, rule application stops and the UCQ ∨M is returned as an FO-rewriting of A0 under T ′ .

T ′ illustrates that the algorithm is incomplete without the minimization step since this step prevents generation of the blocked concept D3.

We now establish correctness and termination.

Theorem 4. The algorithm in Figure 1 returns a UCQrewriting ∨ M if A0 is FO-rewritable under T and the full signature and 'not FO-rewritable' otherwise.

The generated UCQ-rewritings are not necessarily of minimal size. It is possible to attain minimal-size rewritings by using a stronger form of minimality when constructing the concept D′ , namely by redefining the relation "≺" so that C ⪯ D if there is a root-preserving homomorphism from C to D (c.f. most-general rewritings in [K¨onig et al., 2012]). As a consequence, the ≺-minimal concept D′ with T |= D′ ⊑ A can then be of size exponential in the size of D. However, D′ can still be constructed in output-polynomial time.

We prove in the appendix that all concepts in M have outdegree at most n and depth at most 22n , n the size of T . As remarked in [Bienvenu et al., 2013], the size of UCQrewritings can be triple exponential in the size of T , and thus the same is true for the runtime of the presented algorithm. While this worst case is probably not encountered in practice, the size of M can become prohibitively large for realistic inputs. For this reason, we propose an improved algorithm in the subsequent section, which produces non-recursive datalog rewritings instead of UCQ-rewritings and whose runtime is at most single exponential.

4 ADecomposed Algorithm

The algorithm presented in this section consists of three phases. In Phase 1, a set Γ is computed that can be viewed as a decomposed representation of the set M from Section 3 in the sense that we store only single nodes of the tree-shaped concepts inM, rather than entire concepts. In many cases, we can already construct a non-recursive datalog rewriting after Phase 1. If this is not possible, we compute in Phase 2 a set Ω that enriches the node representation provided by Γ with sets of logical consequences that are relevant for Point 2 of the definition of blocked concepts. In Phase 3, we first execute a certain cycle check on Ω, which corresponds to checking the existence of a blocked concept in M. If no cycle is found, we then construct a non-recursive datalog rewriting.

Phase 1. Assume that T is a TBox, Σ an ABox-signature, and A0 a concept name for which we want to compute an FO-rewriting under T and Σ. To present the algorithm, it is convenient to decompose conjunctions on the right-hand side of CIs, that is, to assume that T consists, apart fromRIs, only of CIs of the form C ⊑ A with A a concept name and C ⊑ ∃r.D. We start with describing the construction of a set Γ, whose elements we call node pairs. A node pair has the form (C, S), where C ∈ sub(T ), and S ⊆ sub(T ) is a set of concept names and concepts of the form ∃r.C. Intuitively, a node pair (C, S) describes a set of concepts D such that T |=D ⊑ C and the following conditions are satisfied:

• (i) the concept names that are tlcs of D are S ∩NC;
• (ii) the existential restrictions that are the tlcs of D are obtained from the existential restrictions in S by replacing each ∃r.E ∈ S with some ∃s.E′ such that T |= ∃s.E′ ⊑ ∃r.E.

The computation of Γ starts with {(A0, {A0})} and proceeds by exhaustively applying the following two rules:

• (r1) if (C, S) ∈ Γ, D ⊑ A ∈ T and A ∈ S, then extend Γ with (C, (S \ {A}) ∪ tlc(D)).

After applying either rule, we also have to add the pair (G, tlc(G)) for every subconcept ∃r.G of D to trigger further derivation.

Example 5. Let T = {∃r.(B1 ⊓B2) ⊑ A0, ∃s.B2 ⊑ B2}, and Σ the full signature. Starting with the pair (A0, {A0}) and applying (r1), we extend Γ by (A0, {∃r.(B1 ⊓ B2)}) and ((B1 ⊓ B2), {B1,B2}). (r1) is now applicable to the latter, yielding ((B1 ⊓ B2), {B1, ∃s.B2}) and (B2, {B2}). Another application of (r1) results in e. g. (B2, {∃s.B2}) being added.

From Γ we can extract a (potentially infinitary) UCQ-rewriting of A0 under T and Σ, as follows. Start with defining ΓΣ to be the set of all (C, S) ∈ Γ such that S∩NC ⊆ Σ. Then ̂ΓΣ is obtained as the limit of the sequence of sets ̂Γ0Σ, ̂Γ1Σ, . . . defined as follows:

• ̂Γ0Σ := {(C,⊓S) | (C, S) ∈ ΓΣ and S ⊆ NC}.
• ̂Γi+1 Σ is ̂ΓiΣ extendedwith all pairs (C,D) such that there is (C, S) ∈ ΓΣ with the following property: for each ∃r.G ∈ S there are (G, Cr,G) ∈ ̂ΓiΣ and sr,G ∈ Σ such that T |= sr,G ⊑ r and

Note that if (C,D) ∈ ̂ΓΣ, then D uses only symbols from Σ. The set ̂ΓΣ represents a UCQ-rewriting as follows.

Proposition 6 (Soundness and Completeness of ̂ΓΣ). For all Σ-ABoxes A and a ∈ ind(A), we have A, T |= A0(a) iff there is an (A0, D) ∈ ̂ΓΣ with A |= D(a).

ΓΣ provides us with a sufficient condition for FO-rewritability of A0 under T and Σ and suggests a way to (sometimes) produce a non-recursive datalog rewriting. In fact, if ΓΣ is acyclic in the sense that the directed graph

contains no cycle, then ̂ΓΣ is finite and we obtain a nonrecursive datalog programΠΓΣ that is a rewriting of A0 under T and Σ by taking the rule

for each (C, S) ∈ ΓΣ and using PA0 as the goal predicate. Note that the disjunctions can be removed by introducing auxiliary (monadic) IDB predicates, without causing a significant blowup. If ΓΣ is acyclic, we output the above rewriting. Note that it is potentially much smaller than a UCQ-rewriting since it implements structure sharing. However, if ΓΣ is not acyclic, then A0 could still be FO-rewritable under T and Σ, but the above programwill be recursive.

Example 5 (continued). ΓΣ contains the node pairs (A0, {∃r.(B1 ⊓ B2}), (B1 ⊓ B2, {B1, B2}), (B2, {∃s.B2}) and is thus cyclic. This is the expected outcome since, as argued in Example 3, A0 is not FO-rewritable under T and Σ

Now, let T ′ := T ∪ {B1 ⊑ B2} as in the second part of Example 3. The resulting ΓΣ still contains the above node pairs and is thus cyclic. To find out that A0 is FO-rewritable under T ′ and Σ, the algorithm enters Phase 2.

Phase 2. In the second phase of the algorithm, we construct a set of node tuples ΩΣ by further annotating (and duplicating) the pairs in ΓΣ. A node tuple takes the form t = (Ct, St, cont, Et, xcont) where Ct and St have the same form as the components of node pairs in ΓΣ, Ct ∈ cont ⊆ sub(T ), Et is the special symbol "-" or of the form ∃s.C such that ∃r.C ∈ St for some r with T |= s ⊑ r, and xcont is a subset of cont or "-". Intuitively, a node tuple t ∈ ΩΣ describes a set of concepts D such that (Ct,D) ∈ ̂ΓΣ and apart from (i) and (ii) above the following additional conditions are satisfied:

• (iii) T |= D ⊑ E iff E ∈ cont, for each E ∈ sub(T );
• (iv) if Et = ∃s.C, then there is a tlc ∃s.E in D and a leaf node in E such that (C, E) ∈ ̂ΓΣ and for the concept D′ obtained from D by dropping this node, we have T |= D′ ⊑ E iff E ∈ xcont, for each E ∈ sub(T ).

When St contains no existential restrictions, we use "-" for Et and xcont. To understand Et, it is useful to think of D as a tree and of Et as a selected successor of the root of that tree. We start the construction of ΩΣ with setting

where for a set of concepts M, conT (M) denotes the set of concepts D ∈ sub(T ) such that T |= ⊓M ⊑ D. We call the tuples in the set above leaf tuples. The final set ΩΣ is constructed by exhaustively applying the following rule:

(rΩ) If t = (Ct, St, cont,Et, xcont) is a node tuple with ∃r0.D0, . . . , ∃rn.Dn the existential restrictions in St (n ≥ 0) and there are role names s0, . . . , sn ∈ Σ and node tuples t0, . . . , tn ∈ ΩΣ and an ℓ ∈ {0, . . . , n} such that the following conditions are satisfied, then add t to ΩΣ:

1. T |= si ⊑ ri and Cti =Di for 0 ≤ i ≤ n;
2. Et = ∃sℓ.Dℓ;
3. there is a node pair (Ct, S) ∈ ΓΣ with St ⊆ S and S ∩ NC = St ∩ NC;
4. cont = conT (M), where

1. xcont = conT (M ′ ), where

In Point 5, ∃r.- is identified with ⊤. For t, t′ ∈ ΩΣ, we write t ⇝ΩΣ t′ if there are t0, . . . , tn ∈ ΩΣ that satisfy the conditions listed in (rΩ) and such that t′ = tℓ, that is, t′ is the tuple that was chosen for the selected successor.

Example 5 (continued). For the TBox T , ΩΣ is initialized to

(rΩ) can be applied using (A0, {∃r.(B1 ⊓ B2)}) ∈ ΓΣ for (Ct, S) in Point 3, with n = ℓ = 0, s0 = r, and t0 = tc, adding to ΩΣ the following node tuple t:

We now have t ⇝ΩΣ tc. Note that M = {∃r.B1 ⊓ B2} in Point 4 and that M ′ = ∅ in Point 5, resulting in xcont = ∅.

Phase 3. The third and last phase of the algorithm first checks whether an FO-rewriting exists at all and, if so, produces a rewriting that takes the form of a non-recursive monadic datalog program.

We start with introducing the relevant notion of a cycle. A tuple t ∈ ΩΣ is a root tuple if Ct = A0, A0 ∈ cont and A0 /∈ xcont. A path through ΩΣ is a finite sequence of node tuples t1, . . . , tk from ΩΣ such that ti ⇝ΩΣ ti+1 for 1 ≤ i < k. A tuple t ∈ ΩΣ is looping if there is a path t1, . . . , tk through ΩΣ such that k > 1, t = t1, cont = contk , and xcont = xcontk . We say that ΩΣ contains a root cycle if there are tuples t, t′ ∈ ΩΣ such that t is a root tuple, t′ is a looping tuple, and t′ is reachable from t along⇝ΩΣ .

Theorem 7. A0 is not FO-rewritable under T and Σ if and only if ΩΣ contains a root cycle.

Example 5 (continued). After completing Phase 2 for T , the algorithm checks ΩΣ for cyclicity and finds a root cycle:

The last node tuple possesses a reflexive ⇝ΩΣ edge and leads to the root cycle.

For the TBox T ′ , the second tuple in this path will have {B1 ⊓B2, B1, B2} as xcont (we do not need the selected successor to infer B2 here), and the first tuple above will contain A0 in xcont and will therefore not be a root tuple. Indeed, for T ′ the resulting set ΩΣ does not contain a root cycle.

As suggested by Theorem 7, our algorithm first checks whether ΩΣ contains a root cycle and, if so, returns 'not FO-rewritable'. Otherwise, it constructs a datalog program ΠA0,T that is a rewriting of A0 under T and non-recursive iff A0 is FO-rewritable under T and Σ (which is guaranteed at this point by Theorem 7).

The IDB relations of ΠA0,T take the form PC,con,XCON where C ∈ sub(T ), con is a subset of sub(T ) and XCON is a set of such subsets or the special set {-}. We start with rules

for all t ∈ Ω with St ⊆ NC (which are of the form (Ct, St, cont, -, -)) and then exhaustively add a rule

for all t ∈ Ωwith existential restrictions ∃r0.D0, . . . , ∃rn.Dn the existential restrictions in St, tuples t0, . . . , tn ∈ Ω, role names s0, . . . , sn ∈ Σ, ℓ ∈ {0, . . . , n}, and sets XCON0, . . . , XCONn such that

1. Conditions 1 to 5 from the rule (rΩ) hold;
2. PCti ,conti ,XCONi already occurs in ΠA0,T , for all i ≤ n;
3. XCON consists of all sets conT (M ′ ) such that there is an ℓ′ ≤ n and an xcon ∈ XCONℓ′ with

In Point 3 above, we again identify ∃r.- with ⊤. The goal predicates of ΠA0,T are the predicates of the form PA0,con,XCON with A0 ∈ con and A0 /∈ xcon for all xcon ∈ XCON. To eliminate 'accidental' recursiveness from ΠA0,T , remove all rules that contain a predicate which is not reachable from a goal predicate (defined in the obvious way).

Theorem 8.

1. The programΠA0,T is a rewriting of A0 under T .
2. If A0 is FO-rewritable under T and Σ, then ΠA0,T is non-recursive.

Note that ΠA0,T is of double exponential size in the worst case. It is possible to find a (monadic) program that is only single exponential in the worst case, but unlike the program ΠA0,T it is also best-case exponential. This cannot be significantly improved without giving up monadicity.

Theorem 9. If A0 is FO-rewritable under T and Σ, then it has a monadic non-recursive datalog rewriting of size at most 2p(n) , n the size of T and p() a polynomial.

There is a family of TBoxes T1, T2, . . . such that for all n ≥ 1, Tn is of size O(n2 ), the concept name A0 is FOrewritable under Tn, and the smallest non-recursive monadic datalog rewriting has size at least 2n .

Let us briefly analyze the complexity of the decomposed algorithm. It is easy to verify that the number of Γ-pairs and Ω-tuples is singly exponential in the size of T and that all required operations for building Γ and Ω and for determining the existence of a root cycle require only polynomial time. By Theorem 7, we have thus found an EXPTIME algorithm for deciding FO-rewritability of concept queries under ELTBoxes and ABox signatures, which is optimal [Bienvenu et al., 2013].

5 Experiments

We have implemented the decomposed algorithm in the Grind system and conducted a number of experiments. The system can be downloaded from http://www.informatik.unibremen.de/∼hansen/grind, and is released under GPL. In the following, we point out some selected aspects of the implementation. We use numbers to represent subconcepts in T , store the S-component of each pair (C, S) ∈ Γ, which is a set of subconcepts of T , as an ordered set, and use tries as a data structure to store Γ. We remove pairs (C, S) ∈ Γ where S is not minimal, that is, for which there is a (C, S′ ) ∈ Γ with S′ ⊊ S. It can be verified that this optimization does not compromise correctness. We eagerly check for cycles in Γ without waiting for Phase 1 to complete and immediate start Phase 2 once a cycle is found to check whether it gives raise to non-FO-rewritability. If this is not the case, we return to Phase 1.

The experiments were carried out on a Linux (3.2.0) machine with a 3.5 GHz quad-core processor and 8 GB of RAM. Although a large number of ELHdr -TBoxes is available on the web and from various repositories, most of them are acyclic TBoxes in the traditional DL sense, that is, the lefthand sides of all CIs are concept names, there are no two CIs with the same left-hand side, and there are no syntactic cycles.

Since concept queries are always FO-rewritable under such TBoxes [Bienvenu et al., 2012a], they are not useful for our experiments. We have identified seven TBoxes that do not fall into this class, listed in Table 1 together with the number of concept inclusions (CI), concept names (CN), and role names (RN) that they contain. Role inclusions occur in MOHSE, not-galen, and SO. All TBoxes together with information about their origin are available at http://www.informatik.unibremen.de/∼hansen/grind. All experiments conducted were using the full ABox signature (which in practice is the most difficult case since smaller signatures result in fewer node pairs and node tuples).

For each of these TBoxes, we have applied the decomposed algorithm to every concept name in the TBox. In some rare cases, either the set Γ has reached excessive size or calculation of Ω took too long, resulting in non-termination. We have thus established a 30 second timeout which results in termination in almost all cases; the "stop" column of Table 1 shows the fraction of inputs on which the algorithm successfully terminated, and the "time" column lists the overall runtime needed to process all concept names from the ontology (including timeouts). The generated non-recursive datalogrewritings are typically of very reasonable size. The number of rules in the rewriting is displayed in the upper part of Figure 2; for example, for NBO, about 55% of all rewritings consist of a single rule, about 18% have two or three rules, about 10% have 4-7 rules, and so on. Note that the x-axis has exponential scale. The size of the rule bodies is typically very small, between one and two atoms in the vast majority of cases, and we have never encountered a rule with more than ten body atoms. It is also interesting to consider the number of IDB predicates in a rewriting, as intuitively these correspond to views that have to be generated by a database system that executes the query. As shown in the lower part of Figure 2, this number is rather small, and considerably lower than the number of rules in the produced programs (we again use exponential scale on the x-axis).

The experiments also confirm our initial belief that ontologies which are used in practical applications have a simple structure. As shown in the "no" column of Table 1, the number of concept names that are not FO-rewritable is extremely small. Moreover, if a concept name was FO-rewritable, then we were always able to find a rewriting already in Phase 1 of our algorithm. Note, though, that for those cases that turned out to be not FO-rewritable, we had to go through Phases 2 and 3.

We have also compared the performance of Grind with that of REQUIEM, which implements an incomplete resolutionbased approach to computing FO-rewritings for ontology languages up to ELHI [P´erez-Urbina et al., 2010]. We use the same 30s timeout, which resulted in the termination rate and overall runtime (again including timeouts) displayed in the columns of Table 1 marked with "RQ". The termination cases correspond to positive answers, as REQUIEM cannot determine that an input is not FO-rewritable. Since REQUIEM tends to terminate only on relatively simple inputs, the constructed rewritings of the two tools are often identical. When they are not, either tool may produce a shorter rewriting.

6 Outlook

As future work, we plan to extend the algorithm and implementation from concept queries to conjunctive queries and to more expressive Horn-DLs such as ELHI and Horn-SHIQ. This is non-trivial for several reasons; for example, with inverse roles the computation of the con and xcon sets in Phase 2 is no longer as straightforward as for ELHdr .