Deciding FO-Rewritability in E L

Abstract

We consider the problem of deciding, given an instance query A(x), an E L-TBox T , and possibly an ABox signature , whether A(x) is FO-rewritable relative to T and -ABoxes. Our main results are PSPACE-completeness for the case where comprises all symbols and EXPTIME-completeness for the general case. We also show that the problem is in PTIME for classical TBoxes and that every instance query is FO-rewritable into a polynomial-size FO query relative to every (semi)-acyclic TBox (under some mild assumptions on the data).

Introduction

Over the last years, query answering over instance data has developed into one of the most prominent problems in description logic (DL) research. Many approaches aim at utilizing relational databases systems (RDBMSs), exploiting their mature technology, advanced optimization techniques, and the general infrastructure that those systems offer. Roughly, RDBMS-based approaches can be classified into query rewriting approaches, where the original query and the DL TBox are compiled into an SQL query that is passed to the RDBMS for execution [ 5 ], and combined approaches, where the consequences of the TBox are materialized in the data in a compact form and some query rewriting is used to ensure correct answers despite the compact representation [ 12, 11 ]. This division is by no means strict, as illustrated by the approach presented in [ 7 ] which is based on query rewriting, but also has strong similarities with combined approaches.

A fundamental difference between the query rewriting approach and the combined approach is that, in query rewriting, an exponential blowup of the query is often unavoidable [ 8 ] while the combined approach typically blows up both query and data only polynomially [ 12, 11 ]. It is thus unsurprising that query execution is more efficient in the combined approach than in the query rewriting approach, see the experiments in [ 11 ]. Depending on the application, however, there can still be good reasons to use pure query rewriting. Ease of implementation: Query rewriting approaches are often easier to implement as they do not involve a data completion phase. When the TBox is sufficiently small so that the exponential blowup of the query is not prohibitive or when only a prototype implementation is aimed at, it may not be worthwhile to implement a full combined approach. Access limitations: If the user does not have permission to modify the data in the database, materializing the consequences of the TBox in the data might simply be out of the question. This problem arises notably in information integration applications.

In this paper, we are interested in TBoxes formulated in the description logic E L, which forms the basis of the OWL EL fragment of OWL 2 and is popular as a basic language for large-scale ontologies. In general, query rewriting approaches are not applicable to E L because instance query answering in this DL is PTIME-complete regarding data complexity while AC0 data complexity marks the boundary of DLs for which the pure query rewriting approach can be made work [ 5 ]. For example, the query A(x) cannot be answered by an SQL-based RDBMS in the presence of the very simple E L-TBox T = f9r:A v Ag, 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. We say that A(x) is not FO-rewritable relative to T , alluding to the known equivalence of first-order (FO) formulas and SQL queries.

Of course, such an isolated example does not rule out the possibility that some E LTBoxes, including those that are used in applications, still enjoy FO-rewritability. For example, the query A(x) is FO-rewritable relative to the E L-TBox T 0 = fA v 9r:Ag: since the additional instances of A stipulated by T 0 are ‘anonymous objects’ (nulls in database parlance) rather than primary data objects, there is no unbounded propagation through the data and, in fact, we can simply drop T 0 when answering A(x). Inspired by these observations, the aim of this paper is to study FO-rewritability on the level of individual TBoxes, essentially following the non-uniform approach initiated in [ 15 ]. In particular, we are interested in deciding, for a given instance query (IQ) A(x) and E LTBox T , whether q is FO-rewritable relative to T . Sometimes, we additionally allow as a third input an ABox-signature that restricts the symbols which can occur in the data [ 2, 3 ].

Our main result is that deciding FO-rewritability of IQs relative to general E LTBoxes (sets of concept inclusions C v D) is PSPACE-complete when the ABox signature is full (i.e., all symbols are allowed in the ABox) and EXPTIME-complete when is given as an input. For proving these results, we establish some properties that are of independent interest, such as: (1) whenever an IQ is FO-rewritable, then it is FOrewritable into a union of tree-shaped conjunctive queries; (2) an IQ is FO-rewritable relative to all ABoxes iff it is FO-rewritable relative to tree-shaped ABoxes (see Section 3 for a precise formulation). We also study more restricted forms of TBoxes, showing that FO-rewritability of IQs relative to classical TBoxes (sets of concept definitions A C and concept implications A v C with A atomic, cycles allowed) is in PTIME, even when is part of the input. For semi-acyclic TBoxes T (classical TBoxes without cycles that involve only concept definitions, but potentially with cycles that involve at least one concept inclusion), we observe that every IQ is FO-rewritable relative to T (for any ABox signature ) and that, under the mild assumption that the admitted databases have domain size at least two, even a polynomial-sized rewriting is possible. While it is not our primary aim in this first publication to actually generate FO-rewritings, we note that all our results come with effective procedures for doing this (the rewritings are of triple-exponential size in the worst case).

Although we focus on simple IQs of the form A(x), all results in this paper also apply to instance queries of the form C(x) with C an E L-concept. The treatment of conjunctive queries (CQs) is left for future work. We also discuss the connection of FOrewritability in E L to boundedness in datalog and in the -calculus. Proof details are deferred to the long version at at http://www.informatik.uni-bremen.de/ clu/papers/.

Preliminaries

We remind the reader that E L-concepts are built up from concept names and the concept > using conjunction C u D and existential restriction 9r:C. When we speak of a TBox without further qualification, we mean a general TBox, i.e., a finite set of concept inclusions (CIs) C v D. Other forms of TBoxes will be introduced later as needed. 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. We use Ind(A) to denote the set of all individual names used in A. It will sometimes be convenient to view an ABox A as an interpretation IA, defined in the obvious way (see [ 15 ]).

Regarding query languages, we focus on instance queries (IQ), which have the form A(x) with A a concept name and x a variable. We write T ; A j= A(a) if aI 2 AI for all models I of T and A and call a 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 . To define FO-rewritability, we require first-order queries (FOQs), which are first-order formulas constructed from atoms A(x), r(x; y), and x = y. We use ans(I; q) to denote the set of all answers to the FOQ q in the interpretation I.

A signature is a set of concept and role names, which are uniformly called symbols in this context. A -ABox is an ABox that uses only concept and role names from . The full signature is the signature that contains all concept and role names. Definition 1 (FO-rewritability). Let T be an E L-TBox and an ABox signature. An IQ q is FO-rewritable relative to T and if there is a FOQ ' such that certT (A; q) = ans(IA; ') for all -ABoxes A. Then ' is an FO-rewriting of q relative to T and . Example 1. Recall from the introduction that A(x) is not FO-rewritable relative to T = f9r:A v Ag and the full signature. If we add 9r:> v A to T , then A(x) is FO-rewritable relative to the resulting TBox and the full signature, and '(x) = A(x) _ 9y r(x; y) is an FO-rewriting. If we choose = fAg, then A(x) becomes FO-rewritable also relative to the original T , with the trivial FO-rewriting A(x). Conversely, if a query q is FO-rewritable relative to a TBox T 0 and a signature , then q is FO-rewritable relative to T 0 and any 0 (take an FO-rewriting relative to T 0 and and replace all atoms which involve predicates that are not in 0 with false).

Sometimes, instance queries have the more general form C(x) with C an E Lconcept. Since C(x) is FO-rewritable relative to T and whenever A(x) is FOrewritable relative to T [ fA Cg and , A a fresh concept name, queries of this form are captured by the results in this paper. 3

General TBoxes – Upper Bounds

We first characterize failure of FO-rewritability of an IQ A(x) relative to a TBox T and an ABox signature in terms of the existence of certain -ABoxes and then show how to decide the latter. The following result provides the starting point. An ABox is called tree-shaped if the directed graph (Ind(A); f(a; b) j r(a; b) 2 Ag) is a tree and r(a; b); s(a; b) 2 A implies r = s. A FOQ is a tree-UCQ if it is a disjunction q1 _ _ qn and each qi is a conjunctive query (CQ) that is tree-shaped (defined in analogy with tree-shaped ABoxes) and where the root is the only answer variable; see e.g. [ 15 ] for details on CQs.

Theorem 1. Let T be an E L-TBox,

an ABox signature, and A(x) an IQ. Then 1. If A(x) is FO-rewritable relative to T and , then there is a tree-UCQ that is an

FO-rewriting of A(x) relative to T and ; 2. If '(x) is an FO-rewriting of A(x) relative to T and tree-shaped -ABoxes and '(x) is a tree-UCQ, then '(x) is an FO-rewriting relative to T and ; 3. A(x) is FO-rewritable relative to T and iff A(x) is FO-rewritable relative to T and tree-shaped -ABoxes.

Of the three points in Theorem 1, Point 1 is most laborious to prove. It involves applying an Ehrenfeucht-Fra¨ısse´ game and explicitly constructing a tree-UCQ as a disjunction of certain E L-concepts (c.f. the characterization of FO-rewritability in terms of datalog boundedness given in [ 15 ] and its proof). Point 2 can then be derived from Point 1, and Point 3 is an immediate consequence of Points 1 and 2.

For a tree-shaped ABox A and k 0, we use Ajk to denote the restriction of A to depth k. The following provides the first version of the announced characterization of FO-rewritability in terms of the existence of certain ABoxes.

Theorem 2. Let T be an E L-TBox, an ABox signature, and A(x) an IQ. Then A(x) is not FO-rewritable relative to T and iff for every k 0, there is a tree-shaped -ABox A of depth exceeding k with root a0 s.t. T ; A j= A(a0) and T ; Ajk 6j= A(a0). The proof of Theorem 2 builds on Point 1 of Theorem 1. Note that if A(x) is FOrewritable relative to T and , then there is a k 0 such that for all tree-shaped ABoxes A of depth exceeding k with root a0, T ; A j= A(a0) implies T ; Ajk j= A(a0). In the proof of Theorem 2, we explicitly construct FO-rewritings which are tree-UCQs of outdegree at most jT j and depth at most k.

To proceed, it is convenient to work with TBoxes in normal form, where all CIs must be of one of the forms A v B1, A v 9r:B, > v A, B1 u B2 v A, 9r:B v A with A; B; B1; B2 concept names. This can be assumed without loss of generality: Lemma 1. For any E L-TBox T , ABox signature , and IQ A(x), there is a TBox T 0 in normal form such that for any FOQ ', we have that '(x) is an FO-rewriting of A(x) relative to T and iff '(x) is an FO-rewriting of A(x) relative to T 0 and . To exploit Theorem 2 for building a decision procedure for FO-rewritability, we impose a bound on k. The next theorem is proved using Theorem 2 and a pumping argument. Theorem 3. Let T be an E L-TBox in normal form, an ABox signature, A(x) an IQ, and n = j(sig(T ) [ ) \ NCj. Then A(x) is not FO-rewritable relative to T and iff there exists a tree-shaped -ABox A of depth exceeding 2n with root a0 such that T ; A j= A(a0) and T ; Aj2n 6j= A(a0).

Note that, with the remark after Theorem 2, we obtain a triple exponential upper bound on the size of FO-rewritings. The bound in Theorem 3 is optimal in the sense that, for every n 1, there is an E L-TBox T and an IQ A(x) such that jsig(T ) \ NCj = n, A(x) is FO-rewritable relative to T and the full , and for all ABoxes of depth at least 2n with root a0, we have T ; A j= A(a0) iff T ; Aj2n 1 j= A(a0). Such a T can be constructed by simulating a binary counter, see Section 4 of [ 13 ]. Based on Theorem 3, we can establish the following result.

Theorem 4. Deciding FO-rewritability of an IQ relative to an E L-TBox and an ABox signature is in EXPTIME.

The proof utilizes non-deterministic bottom-up automata on finite, ranked trees: we construct exponential-size automata that accept precisely the ABoxes A from Theorem 3 and then decide their emptiness in PTIME.

When is full, the characterization given in Theorem 3 can be further improved. An ABox A is linear if it consists of role assertions r0(a0; a1); : : : ; rn 1(an 1; an) and concept assertions A(a) with a 2 fa0; : : : ; ang. Somewhat unexpectedly, with full we can replace the tree-shaped ABoxes from Theorem 3 with linear ones. Theorem 5. Let T be an E L-TBox in normal form, A(x) an IQ, and n = j(sig(T ) [ ) \ NCj. Then A(x) is not FO-rewritable relative to T (and the full ) iff there exists a linear ABox A of depth exceeding 2n with root a0 such that T ; A j= A(a0) and T ; Aj2n 6j= A(a0).

The surprisingly subtle proof of Theorem 5 is based on the careful extraction of a linear ABox from the tree-shaped one whose existence is guaranteed by Theorem 3. The subtlety is largely due to the fact that it is not sufficient to simply select a linear chain of individuals from the tree-shaped ABox; additionally, the concept assertions on that chain have to be modified in a very careful way.

The following example shows that, when is not full, tree-shaped ABoxes in Theorem 3 cannot be replaced with linear ones.

Example 2. Let T = fAi v Xi; Bi u Xi v Yi; 9r:Yi v Xi j i 2 f1; 2gg [ fX1 u X2 v X; B1 u B2 v Z; 9r:Z v Xg; = fA1; A2; B1; B2; rg, and take the IQ X(x). The tree-shaped ABox A = fr(a0; ai;0); r(ai;0; ai;1); : : : ; r(ai;2n 1; ai;2n ) j i 2 f1; 2gg [

fB(ai;0); : : : ; B(ai;2n ); Ai(ai;2n ) j i 2 f1; 2gg; with n as in Theorems 3 and 5, is of depth exceeding 2n and it can be verified that T ; A j= X(a0), but T ; Aj2n 6j= X(a0). However, for all linear -ABoxes A, we have T ; A j= X(a0) iff T ; Aj1 j= X(a0).

Theorem 5 allows us to replace the non-deterministic tree automata in the proof of Theorem 6 with word automata, improving the upper bound to PSPACE. Theorem 6. Deciding FO-rewritability of an IQ relative to an E L-TBox and the full ABox signature is in PSPACE.

General TBoxes – Lower Bounds

We establish lower bounds that match the upper bounds from the previous section. Theorem 7. Deciding FO-rewritability of an IQ relative to a general E L-TBox and an ABox signature is (1) PSPACE-hard when is full and (2) EXPTIME-hard when is an input.

The proof of Point 1 is by reduction of the word problem of polynomially spacebounded deterministic Turing machines (DTMs). For Point 2, we modify the proof of Point 1 to yield a reduction of the word problem of polynomially space-bounded alternating Turing machines (ATMs). We start with the former.

Let M = (Q; ; ; ; q0; qacc; qrej) be a DTM and p( ) its polynomial space bound. We assume w.l.o.g. that M terminates on every input, that it never attempts to move left on the left-most end of the tape, that q0 2= fqacc; qrejg, and that there are no transitions defined for qacc and qrej. Let x 2 be an input to M of length n. Our aim is to construct a TBox T and select a concept name B such that B is not FO-rewritable relative to T and the full signature iff M accepts x.

By Theorem 5, non-FO-rewritability of B w.r.t. T is witnessed by a sequence of linear ABoxes of increasing depth. In the reduction, these ABoxes take the form of longer and longer r-chains (with r a role name). The chains represent the computation of M on x, repeated over and over again. Specifically, the tape contents, the current state, and the head position are represented using the elements of [ ( Q) as concept names. If, for example, x = ab and the computation of M on x consists of the two configurations qab and aq0b,4 then this is represented by ABoxes of the form fr(b0; b1); r(b1; b2); r(b2; b3); : : : ; r(bn 1; bn)g where additionally, the concept (q; a) is asserted for b0; b4; b8; : : : , a is asserted for b1; b5; b9; : : : and for b2; b6; b10; : : : , and (q0; b) for b3; b7; b11; : : : . If M accepts x, then B is propagated backwards along these chains (from b0 to b1 to b2 etc) unboundedly far, starting from a single explicit occurrence of B asserted for b0. If M rejects x or the chain in the ABox does not properly represent the computation of M on x, then B will already be implied by any subchain of length at most p(n)2 and thus the unbounded propagation of B gets ‘disrupted’ resulting in FO-rewritability of B relative to T .

The following CI in T results in backwards propagation of B provided that every ABox individual is labeled with at least one symbol from Q: [ 9r:(A u B) v B for all A 2 [ (

Q): (1) Disrupt the propagation of B when M does not accept x: (a; qrej) v B for all a 2 : We have to enforce that the ABox actually represents a (repeated) computation of M . To do this, we again use disruptions of the propagation of B: whenever an ABox A 4 uqv 2 Q means that M is in state q, the tape left of the head is labeled with u, and starting from the head position, the remaining tape is labeled with v. represents a configuration sequence that is not a proper computation, then B is implied by a sub-chain of bounded length. Let forbid denote the set of all tuples (A1; A2; A3; A) with Ai 2 [( Q) such that whenever three consecutive tape cells in a configuration c are labeled with A1; A2; A3, then in the successor configuration c0 of c, the tape cell corresponding to the middle cell cannot be labeled with A. Put

A u 9rp(n)+1:A1 u 9rp(n):A2 u 9rp(n) 1:A3 v B (2) for all (A1; A2; A3; A) 2 forbid. This ensures that the transition relation is respected and that the content of tape cells which are not under the head does not change. We also need to say that every tape cell has a unique label, that there is at not more than one head position per configuration, and at least one, again via disrupting the propagation of B:

A u A0 v B for all distinct A; A0 2 9ri:H u 9rj H v B for i < j < p(n) a v H for all a 2 H u 9r:H u u 9rp(n) 1:H v B where H is a concept name indicating that the head is on the current cell and H indicating that this is not the case. It remains to set up the initial configuration. It is tempting to introduce a concept name I that sets up the initial configuration and must be used at the end of the r-chain to start the propagation of B. However, since we assume the ABox signature to be full, we can always put B itself at the end of the chain, avoiding I. To fix this issue, we refrain from introducing I, but utilize the final states qacc and qrej, enforcing that they must always be followed by the initial configuration. Let A(10); : : : ; A(m0) be the concept names that describe the initial configuration, i.e., when the input x is x1 xn, then A(00) = (x1; q0), Ai(0) = xi for 2 is the blank symbol for n < i p(n). Now put i n, and A(0) = xi i 9ri:qacc v A(0) i and 9ri:qrej v A(0) i for 1 i p: (3) Note that all witness ABoxes for non-FO-rewritability of B must eventually contain qacc or qrej, thus the initial configuration will be properly set up at some point: ABoxes A that do not contain these states do not represent a proper computation of M because M reaches qacc or qrej after at most p(n) states, thus the propagation of B is disrupted in A.

We now come to Point 2 of Theorem 7. When the ABox signature is not required to be full, it is much simpler to set up the initial configuration. Indeed, we can then simply introduce the mentioned concept name I, add I v B to T , and set = [ ( Q) [ fr; Ig to ensure that we must use I to start the propagation of B. We can further replace the CIs (3) above with 9ri:I v Ai(0) and 9ri:I v Ai(0) for 1 i p to ensure that I sets up the initial configuration as intended. With this modification, we can adapt the reduction from DTMs to ATMs in a straightforward way, thus improving the PSPACE lower bound to an EXPTIME one. We only give a brief sketch. Assume w.l.o.g. that each configuration of the ATM M has at most two successor configurations. We introduce a second role name s 2 , reserving r for the first successor of a configuration and s for the second successor. Then the CIs (1) are replaced with 9r:(A u B) u 9s:(A0 u B) v B for all A; A0 2 resulting in witness ABoxes to take the form of a tree-shaped ATM computation rather than a linear DTM computation. It remains to adapt the CIs (2) to reflect the branching of computations. The set forbid now contains tuples (A1; A2; A3; A01; A02; A03; A), where A1; A2; A3 describe three neighboring cells in the left predecessor configuration and A01; A02; A03 the corresponding cells in the right predecessor configuration (for existential states of M , we simply assume that the left and right predecessor are identical). We can then replace (2) with A classical TBox T is a finite set of concept definitions A C and CIs A v C where A is a concept name. No concept name is allowed to occur more than once on the left hand side of a statement in T .

Theorem 8. Deciding FO-rewritability of an IQ relative to a classical E L-TBox and an ABox signature is in PTIME.

We give examples illustrating FO-rewritability in classical TBoxes and give the main idea of the proof.

Example 3. (a) The IQ A(x) is not FO-rewritable relative to the classical TBox fA 9r:Ag and the full ABox signature. (b) The concept name A has a cyclic definition in the TBox T = f A B u 9r:A; B v 9r:A g which often indicates non-FO-rewritability, but in this case the IQ A(x) has an FO-rewriting relative to T and the full ABox signature, namely '(x) = A(x) _ B(x). To present the idea of the proof, we use an appropriate normal form for classical TBoxes. A concept name A is defined in T if there is a definition A C 2 T and primitive otherwise; A is non-conjunctive in T if it occurs in T , but there is no CI of the form A B1 u u Bn in T with n 1 and B1; : : : ; Bn concept names. We use non-conj(T ) to denote the set of non-conjunctive concepts in T . A classical TBox T is in normal form if it is a set of statements A 9r:B and A B1 u u Bn where B; B1; : : : ; Bn are concept names and B1; : : : ; Bn are non-conjunctive. For every classical TBox T , one can construct in polynomial time a classical TBox T 0 in normal form that uses additional concept names such that T 0 j= T and every model of T can be expanded to a model of T 0 [ 10 ]. It is not hard to verify that an IQ A(x) is FO-rewritable relative to T and if and only if it is FO-rewritable relative to T 0 and , provided that A is not among the new concept names introduced during the construction of T 0. For a classical TBox T in normal form and a concept name A, define non-conjT (A) = fAg if A is non-conjunctive in T fB1; : : : ; Bng if A B1 u u Bn 2 T : Our polytime algorithm utilizes an ABox introduced in [ 10, 9 ] in the context of conservative extensions and logical difference: given a classical TBox T in normal form and an ABox signature , we compute in polytime a polysize -ABox AT ; with individual names aB, B non-conjunctive in T , such that for any -ABox A, individual name a in A, and concept name A the following conditions are equivalent: – T ; A 6j= A(a); – there exists B 2 non-conjT (A) such that (A; a) is simulated by (AT ; ; aB) (see appendix of long version of this paper).

It follows that to check whether A(x) is FO-rewritable, instead of considering arbitrary tree-shaped -ABoxes A and Ajk as in Theorem 2, it suffices to consider the tree unfolding of AT ; at aB and its restriction to depth k, for all B 2 non-conjT (A). The original search problem has been reduced to the problem of analysing the tree unfolding of AT ; . A polytime algorithm performing that analysis is given in the long version. 6

Semi-Acyclic TBoxes

It is easy to see that every IQ is FO-rewritable relative to every acyclic E L-TBox and every ABox signature . We observe that the same holds for semi-acyclic TBoxes, where some cycles are still allowed, and that it is possible to find rewritings of polynomial size when only databases of domain size at least two are admitted.

A semi-acyclic TBox is defined like a classical TBox, except that definitorial cycles are disallowed, i.e., there cannot be concept definitions A0 C0; : : : ; An 1 Cn 1 such that Ai occurs in Ci+1 mod n. Note that cycles via concept inclusions, such as A v 9r:A, are still permitted. Let T be a semi-acyclic TBox and an ABox signature. For an E L-concept C, we use preT ; (C) to denote the FO-formula WB2 j T j=BvC B(x): For all concept names A and E L-concepts C and D and role names r, set '>;T (x) = true 'A;T (x) = preT ; (A) 'A;T (x) = 'C;T (x) 'CuD;T (x) = 'C;T (x) ^ 'D;T (x) '9r:C;T (x) = preT ; (9r:C) _ 9y:(r(x; y) ^ 'C;T [y=x]) if r 2 '9r:C;T (x) = preT ; (9r:C) where '[x=y] denotes the result of first renaming all bound variables in ' so that y does not occur, and then replacing the free variable x of ' with y.

Lemma 2. For all IQs A(x), 'A;T (x) is an FO-rewriting of A(x) relative to T and . The size of 'A;T (x) can clearly be exponential in the size of T , for example when A = An and T = fAi 9r:Ai 1 u 9s:Ai 1 j 1 i ng. To reduce 'A;T to polynomial size, we can use Avigad’s observation that FO supports structure sharing [ 1 ]. More precisely, let ' be a positive FOQ (such as 'A;T ) whose subformulas if A is primitive if A

C 2 T if r 2= include (x1); : : : ; (xn). The multiple occurences of can be avoided by rewriting ' to 9u8y8z ( (y) $ z = u) ! '0 where '0 is ' with each (xi) replaced with y = xi ! z = u. Intuitively, we iterate over all y and memorize whether (y) holds using identity of z with u. Since we need at least two different ‘values’ for z to make this trick work, the resulting FOQ is an FO-rewriting only on ABoxes with at least two individual names. 7

Related Work

In [ 15 ], deciding FO-rewritability is studied in the context of the expressive DL ALCF I and several of its fragments. In general, though, the setup in that paper is different: while we are interested in deciding FO-rewritability of a single query relative to a TBox, the results in [ 15 ] concern deciding whether, for a given TBox T , all queries are FO-rewritable relative to T . It is shown that this problem is decidable for HornALCF I-TBoxes of depth at most two and for Horn-ALCF -TBoxes (queries are IQs or, equivalently, CQs). As a by-product of these results, a close connection between FO-rewritability of TBoxes formulated in Horn DLs and boundedness of datalog programs is observed, see e.g. [ 6, 17 ] for the latter problem. In its original formulation, the following result is established for a larger class of TBoxes, namely materializable ALCF I-TBoxes of depth one.

Lemma 3 ([ 15 ]). For every (general) E L-TBox T in normal form, there is a datalog program T such that for every ABox signature and IQ A(x), the predicate A is bounded in T relative to -databases iff A(x) is FO-rewritable relative to T and . In [ 15 ], the program T is of exponential size. Since we are only interested in E LTBoxes, it is easy to find a T of polynomial size. More specifically, T consists of A(x) B(x) B(x) B(x) true if > v A 2 T r(x; y); A(x) if 9r:A v B 2 T A1(x); A2(x) if A1 u A2 v B 2 T

X9r:A(x) X9r:A(x) if 9r:B0 v B 2 T and T j= A v B0

B(x) if B v 9r:A 2 T (where possibly A1 = A2) This allows to carry over the 2EXPTIME upper bound for predicate boundedness of connected monadic datalog programs [ 6 ] to FO-rewritability of an IQ relative to a general E L-TBoxes and an ABox signature.5

Note that boundedness has been studied also in the context of the -calculus and monadic second order (MSO) logic [ 16, 4 ]. Here, an EXPTIME upper bound is known from [ 16 ] and it seems likely that this result can be utilized to find an alternative proof of Theorem 6. In particular, it is possible to find a -calculus rewriting ' of an IQ A(x) relative to an E L-TBox T and ABox signature : proceeding similarly to the construction of the above datalog program T , we can find a -calculus formula 'T ; such that for all -ABoxes A and a 2 Ind(A), we have T ; A j= A(a) iff IA; a j= '. When simultaneous fixpoints are admitted, ' even has polynomial size. 5 Note that we explicitly fix the signature of the databases over which boundedness of T is considered instead of assuming that only the EDB predicates can be used in the data as in [ 6 ]; this is only for simplicity and, in fact, it is easy to adapt T to the latter assumption.

Conclusions

It would be interesting to generalize the results presented in this paper to more expressive DLs and to more expressive query languages. Regarding the former, we note that using the techniques in [ 14, 15 ] it is possible to derive a NEXPTIME upper bound for deciding FO-rewritability of IQs relative to Horn-ALCI -TBoxes and ABox signatures. Regarding the latter, CQs are a natural choice and we believe that a mix of techniques from this paper and those in [ 3 ] might provide a good starting point. It is interesting to note that FO-rewritability of all IQ-atoms A(x) in a CQ q does not imply that q is FO-rewritable and the converse fails, too.

Acknowledgements. C. Lutz was supported by the DFG SFB/TR 8 ‘Spatial Cognition’.

References

1. J. Avigad . Eliminating definitions and skolem functions in first-order logic . In Proc. of LICS , pages 139 - 146 . IEEE Computer Society, 2001 .

2. F. Baader , M. Bienvenu , C. Lutz , and F. Wolter . Query and predicate emptiness in description logics . In Proc. of KR . AAAI Press, 2010 .

3. M. Bienvenu , C. Lutz , and F. Wolter . Query containment in description logics reconsidered . In Proc. of KR , 2012 . To appear.

4. A. Blumensath , M. Otto , and M. Weyer . Decidability results for the boundedness problem . Manuscript , 2012 .

5. D. Calvanese , G. De Giacomo, D. Lembo , M. Lenzerini , and R. Rosati . Tractable reasoning and efficient query answering in description logics: The DL-Lite family . J. of Automated Reasoning , 39 ( 3 ): 385 - 429 , 2007 .

6. S. S. Cosmadakis , H. Gaifman , P. C. Kanellakis , and M. Y. Vardi . Decidable optimization problems for database logic programs . In Proc. of STOC , pages 477 - 490 . ACM, 1988 .

7. G. Gottlob and T. Schwentick . Rewriting ontological queries into small nonrecursive datalog programs . In Proc. of DL. CEUR-WS , 2011 .

8. S. Kikot , R. Kontchakov , V. V. Podolskii , and M. Zakharyaschev . Exponential lower bounds and separation for query rewriting . CoRR, abs/1202.4193 , 2012 .

9. B. Konev , M. Ludwig , D. Walther , and F. Wolter . The logical diff for the lightweight description logic E L. Technical report , U. of Liverpool, http://www.liv.ac.uk/ frank/publ/, 2011 .

10. B. Konev , D. Walther , and F. Wolter . The logical difference problem for description logic terminologies . In Proc. of IJCAR , pages 259 - 274 . Springer, 2008 .

11. R. Kontchakov , C. Lutz , D. Toman , F. Wolter , and M. Zakharyaschev . The combined approach to query answering in DL-Lite . In Proc. of KR . AAAI Press, 2010 .

12. C. Lutz , D. Toman , and F. Wolter . Conjunctive query answering in the description logic E L using a relational database system . In Proc. of IJCAI , pages 2070 - 2075 . AAAI Press, 2009 .

13. C. Lutz and F. Wolter . Deciding inseparability and conservative extensions in the description logic E L . In J. of Symbolic Computation 45 ( 2 ): 194 - 228 , 2010 .

14. C. Lutz and F. Wolter . Non-uniform data complexity of query answering in description logics . In Proc. of DL. CEUR-WS , 2011 .

15. C. Lutz and F. Wolter . Non-uniform data complexity of query answering in description logics . In Proc. of KR , 2012 . To appear.

16. M. Otto . Eliminating recursion in the -calculus . In Proc. of STACS , pages 531 - 540 . Springer, 1999 .

17. R. van der Meyden. Predicate boundedness of linear monadic datalog is in PSPACE . Int. J. Found. Comput. Sci. , 11 ( 4 ): 591 - 612 , 2000 .