We study the problem of answering instance queries over non-Horn ontologies by rewriting them into Datalog programs or FirstOrder queries (FOQs). We consider the basic non-Horn language ELU , which extends EL with disjunctions. Both Datalog-rewritability and FOrewritability of instance queries have been recently shown to be decidable for ALC ontologies (and hence also for ELU ); however, existing decision methods are mainly of theoretical interest. We identify two fragments of ELU for which we can compute Datalog-rewritings and FO-rewritings of instance queries, respectively, by means of a resolution-based algorithm.
We study the problem of answering queries over DL ontologies by rewriting them into a First-Order query (FOQ) or a Datalog program. On the theoretical side, rewriting queries into an FOQ or a Datalog program ensures tractability of query answering in terms of data complexity. On the practical side, it allows one to reuse optimised data management systems, namely RDBMSs in the case of FOQs and rule-based systems such as OWLim or Oracle's Semantic Data Store in the case of Datalog.
The problem of ontology-based query answering via query rewriting has so far been mainly studied for Horn DLs. FO-rewritability is ensured for logics of the DL-Lite family [5] and query rewriting algorithms in these DLs have been implemented in systems such as QuOnto [1], Presto [17], Quest [16], Rapid [6], and Owlgres [20]. Datalog rewritability is ensured for logics of the E L family, as well as more expressive languages such as Horn-SHIQ [11]; optimised algorithms have been implemented in systems such as Requiem [15] and Clipper [10]. FOrewritability has also been studied as a decision problem for logics of the E Lfamily [3], where tight complexity bounds have been shown.
Horn DLs, however, cannot capture disjunctive knowledge, such as `every student is either a graduate or an undergraduate'. As a consequence, ontologies capturing disjunctive knowledge cannot be processed using existing rewriting techniques. Little is known about how to compute FO and Datalog rewritings for non-Horn ontologies, and rst results have been obtained only recently. Instance queries (i.e., queries of the form A(x) with A a concept name) are known to be FO-rewritable w.r.t. ontologies expressed in certain logics of the DL-Litebool family |the extension of DL-Lite logics with disjunction [2]|, and a goal-oriented resolution algorithm for computing rewritings w.r.t. such logics has been proposed in [8]. In contrast, instance queries w.r.t. ontologies expressed in the basic non-Horn DL E LU are not generally rewritable into Datalog: a result that holds regardless of any complexity-theoretic assumptions [8]. While FO and Datalog rewritability of instance queries w.r.t. ALC ontologies have been proved to be decidable [4], the decision methods in [4] are problematic in practice as their rst step, translation to CSP, has exponential best-case complexity. Finally, for certain classes of conjunctive queries, query answering over non-Horn ontologies can be reduced to knowledge base consistency [13]. This approach, however, does not generally ensure tractability in terms of data complexity.
In this paper, we are interested in ontologies formulated in the basic non-Horn DL E LU . For simplicity, we focus on instance queries of the form A(x). In general, however, our results apply to ground queries, where all variables are required to be mapped to constants; such queries form the basis of the standard query language SPARQL. Our main result is the identi cation of two su cient conditions on E LU -ontologies that ensure FO-rewritability and Datalog rewritability of instance queries, respectively. Furthermore, we provide resolution-based algorithms that can be used for computing the corresponding rewritings in case our su cient conditions are ful lled. Our algorithms build on the generic resolutionbased technique proposed in [8].
This paper is accompanied with an appendix containing the proofs of our technical results. 2
We consider First-Order logic without equality and function symbols. Variables, terms, (ground) atoms, literals, formulae, sentences, intepretations, models and entailment are de ned as usual. An ABox is a nite set of ground atoms (called facts). We also adopt standard notions of (Horn) clauses, (variable) substitutions, and most general uni ers (MGUs). Positive factoring (PF) and binary resolution (BR) are as follows, where is the MGU of atoms A and B:
PF:
C _ A _ B C _ A
BR:
C _ A D _ :B (C _ D)
a clause D if a substitution exists such that each literal in C occurs in D. Furthermore, C -subsumes D if C subsumes D and C has no more literals than D. Clause C is redundant in a set of clauses if C is a tautology or if C is -subsumed by another clause in the set. The condensation of a clause C is the clause D with the least number of literals such that D C and C subsumes D. The Description Logic E LU . We assume familiarity with standard DLs; here, we brie y recapitulate the syntax of E LU . An E LU -concept is an expression of the form >, A, C1 u C2, C1 t C2, or 9R:C, where A is a concept name, C(i) are concepts, and R is a role name. An E LU -TBox T is a nite set of GCIs of the form C1 v C2 where C1 and C2 are E LU -concepts. An E LU -TBox is normalised it it contains only axioms of the form 9R:A v B, A v 9R:B, and dn j=1 Bj , where A(i) and B(j) are either named or >. Each E LU -TBox i=1 Ai v Fm
where tuples of variables x and z are disjoint, '(x; z) is a conjunction of atoms, and (x) is a disjunction of atoms. Formula ' is the body of r, formula is the head of r, and quanti ers in a rule are omitted for brevity. Furthermore, we often abuse notation and treat a rule and its equivalent clause as synonyms. A rule is Datalog if (x) is a single atom, and it is disjunctive otherwise. A (Datalog) program is a nite set of (Datalog) rules. A program is monadic if every predicate occurring in the head of a rule is unary.
An E LU -program consists of the following kinds of rules: (i) Vin=1 Ai(x) ! Wm
j=1 Bj (x) and (ii) R(x; y)^A(y) ! B(x), where the atom A(y) can be omitted.
is linear if conjunction does not occur on the left-hand side of a rule of type (i). Queries. An (instance) query is a unary atom Q(x). A constant c is an answer to Q(x) w.r.t. a set of FO sentences F and an ABox A if F [ A j= Q(c). The set of answers to Q relative to F and A is denoted as cert(Q(x); F ; A).
responding to A in the obvious way. An FO formula '(x) with one free variable is an FO-rewriting of a query Q(x) w.r.t. an E LU -TBox (or, equivalently, an
A: c 2 cert(Q; T ; A) i IA j= '(c). Furthermore, we say that '(x) is a UCQrewriting if it is of the form '(x) = Win=1 'i(x) where each 'i(x) is constructed using only conjuction and existential quanti cation. We say that Q(x) is FOrewritable w.r.t. T if an FO-rewriting of Q(x) w.r.t. T exists. Finally, T is FO-rewritable if for each concept name A in T the query A(x) is FO-rewritable w.r.t. T . A Datalog program P is a rewriting of a query Q(x) relative to a TBox (or, equivalently, an E LU -program) T if cert(Q(x); T ; A) = cert(Q(x); P; A) for every ABox A. We say that Q(x) is Datalog-rewritable w.r.t. T if a Datalog rewriting of Q(x) w.r.t. T exists. Finally, P is a rewriting of T if it is a rewriting for each query A(x) w.r.t. T , with A a concept name in T ; TBox T is Datalogrewritable if a Datalog rewriting of T exists. As observed in [4], it follows from the homomorphism preservation theorem for nite structures [18] that each FOrewritable query is also UCQ rewritable and hence Datalog rewritable as well. 3
We next recapitulate the generic resolution-based technique proposed in [8], which takes a TBox T and attempts to rewrite it into a Datalog program. If T is restricted to be in E LU , this technique consists of the following two steps. Step 1: From DLs to Disjunctive Datalog. First, the algorithm in [12] is applied to transform T into an ELU -program D that entails the same facts as T w.r.t. every ABox. By eliminating the positive occurrences of existential quanti ers, one thus reduces the problem of rewriting the DL TBox T to the problem of rewriting the disjunctive program D.
Step 2: From Disjunctive Datalog to Datalog. Second, the program D is transformed into a Datalog program P using a variant of the mainstream knowledge compilation algorithms proposed in [19] for propositional clauses, and extended in [9] to First-Order clauses (but without termination guarantees). Procedure 1 summarises (a slight variation of) the technique from [9]. Roughly speaking, the procedure applies binary resolution and factoring and keeps only the consequences that are not redundant. Unlike unrestricted resolution, the procedure never resolves two Horn clauses. The main property of Procedure 1 shown in [9] is that, even if it never terminates, each Horn consequence of the input S will also eventually become entailed by SH . In [8], it was shown that
input and the procedure terminates, then the output P is a Datalog rewriting of D. In essence, this result implies that compilation into Horn clauses can be done in an ABox independent way: D and P can be combined with an arbitrary ABox and still entail the same facts.
Example 3.1 We use the ELU -programs D1 and D2 as running examples: D1 = f C(x) ! A(x) _ B(x)
R(x; y) ^ A(y) ! H(x) R(x; y) ^ B(y) ! D(x) R(x; y) ^ D(y) ! H(x) g
D2 = f >(x) ! A(x) _ B(x)
R(x; y) ^ A(y) ! B(x) R(x; y) ^ B(y) ! A(x) g The results proved in [8] imply that DH1 is a Datalog rewriting of D1. In contrast, Procedure 1 does not terminate when given D2 as input. Although the mutually recursive Datalog rules in D2 are never resolved directly with each other, they can interact via the program's (only) disjunctive rule. As a result, Procedure 1 will eventually derive each of the following (in nitely many) rules, for each even number n and for each Z 2 fA; Bg:
R(xn; x0) ^ n ^ R(xi; xi 1) ! Z(xn) i=1 4
Su
cient Conditions for Rewritability
Datalog-rewritability, respectively. Both conditions come with resolution-based algorithms for computing rewritings. To ensure termination of resolution, both our conditions apply to linear E LU -programs only. As we discuss later on in x5, termination in the non-linear case becomes much more problematic, and it is left for future work. 4.1
FO Rewritability As shown by Bienvenu et al. [3], if an instance query A(x) is FO-rewritable w.r.t. an E L-TBox, then there exists a tree-shaped UCQ that is an FO-rewriting for the given query and TBox. This property was critical to the study of FO-rewritability in the context of E L as it implies a characterisation of FO-rewritability in terms of tree-shaped ABoxes. Since only tree-shaped ABoxes are relevant, one can exploit standard tree automata machinery to study the problem.
Once disjunctions come into play, however, this key property seems to break.
that do not seem to be rewritable into tree-shaped UCQs. Thus, the machinery developed in [3] for E L does not seem to extend to E LU .
Example 4.1 The query H(x) is FO-rewritable w.r.t. our example program D1. The following UCQ '(x) = '1(x) _ '2(x) _ '3(x) _ '4(x) _ '5(x) can be obtained by unfolding the Datalog rewriting obtained by Procedure 1 on D1: '1(x) = H(x) '2(x) = 9y: R(x; y) ^ A(y) '3(x) = 9y: R(x; y) ^ D(y) '4(x) = 9y:9z: R(x; y) ^ R(x; z) ^ R(z; y) ^ C(y) '5(x) = 9y:9z: R(x; y) ^ R(y; z) ^ B(z)
shaped UCQ-rewriting as de ned in [3].
tree-shaped rewriting, linearity allows us to restrict resolution proofs in a critical way. We can show that each derivation from D via resolution and condensation only (i.e., no factoring) involves only tree-shaped rules. This implies that each non-tree rule derived by resolution and factoring is a factor of a tree-shaped rule.
antees FO-rewritability. When applied to a program D satisfying the condition (such as D1 in our running example), Procedure 1 will terminate: the size of derived tree-shaped rules will be limited by the size of D. Furthermore, the Datalog program obtained as output will be bounded for every predicate in the standard sense [14]. Our condition is de ned as given next.
De nition 4.2. The dependency graph of a linear E LU -program D is the least directed edge-labeled graph GD = (V; E; ) satisfying the following conditions: 1. each unary predicate occurring in D is a node in V ; 2. (A; B) 2 E \ for each rule in D of the form R(x; y) ^ A(y) ! B(x); 3. (A; Bi) 2 E with i 2 [1; n] for each rule in D of the form A(x) ! Win=1 Bi(x). Edges contained in the labelling are called transfer edges; all remaining edges are called propositional edges. A transfer cycle is a simple cycle that contains at least one transfer edge. The program D is acyclic if GD contains no transfer cycle. Finally, the transfer depth of a unary predicate A in an acyclic program D is the maximal number of transfer edges on a path in GD ending in A. Intuitively, the maximal transfer depth of a predicate in an acyclic program establishes a bound on the role depth of the tree-shaped rules that can be generated by Procedure 1. Termination of Procedure 1 is then ensured by condensation, which bounds the branching factor of rules in terms of their depth. Example 4.3 Consider the program D1 from Example 3.1. The dependency graph for D1 is given next, where transfer edges are dashed. Clearly, D1 is acyclic and predicate H has transfer depth 2.
C
A B
H
Procedure 2 computes a UCQ rewriting of a query A(x) relative to an acyclic program D. On input D and A, we rst apply Procedure 1 to compute a Datalog rewriting P of D; as already seen, termination of this rst step is guaranteed.
(
Theorem 4.4. Given an acyclic E LU -program D and a unary predicate A in D, Procedure 2 terminates and returns a UCQ rewriting of A(x) w.r.t. D. Example 4.5 When applied to the predicate H and the program D1 from Example 3.1, Procedure 2 rst calls Procedure 1, which returns the program DH1 from Example 3.1 as a Datalog rewriting of D1. So, P is initialised with DH1 and P0 is set to fH(x) ! Q(x)g. On these values, unfolding terminates after ve iterations of the main loop with the following rules in P00:
H(x) ! Q(x) R(x; y) ^ A(y) ! Q(x) R(x; y) ^ D(y) ! Q(x)
R(x; z) ^ R(x; y) ^ R(z; y) ^ C(y) ! Q(x)
R(x; y) ^ R(y; z) ^ B(z) ! Q(x) This yields precisely the UCQ '(x) given in Example 4.1. 4.2
Datalog Rewritability
by allowing certain kinds of cyclic programs. Intuitively, we allow programs that can be separated into two parts: one that may contain disjunctive rules but no transfer cycles, and another one that contains only Datalog rules, but may contain transfer cycles. We call such programs separable.
De nition 4.6. Let D be a linear E LU -program and let D_ be the smallest subset of D such that 1. each disjunctive rule in D is contained in D_; and 2. no unary predicate in D n D_ occurs in the body of a rule in D_. Program D is separable if D_ is acyclic.
Example 4.7 Program D2 from our running example 3.1 is not FO-rewritable; however, it is separable: D_2 = f>(x) ! A(x) _ B(x)g and it is therefore acyclic as in De nition 4.2.
We deal with separable programs by eliminating cycles from their Datalog part. Cycle elimination is based on the observation that every linear E L-program
and rules as transitions labeled by binary predicates (or > if the rule contains no binary predicate). Given a unary predicate B in P, an ABox A, and an individual b, every derivation of B(b) from P [ A corresponds to a path ending in B in TP ; hence, paths in TP encode resolution proofs.
The set of all possible derivations of an assertion B(b) from an assertion
deterministic nite automaton constructed from TP by taking A as the unique initial state, and B as the unique accepting state.
De nition 4.8. Let D be a linear E LU -program and let hA; Bi be a pair of unary predicates occurring in D. The automaton for D relative to hA; Bi is the non-deterministic nite word automaton AutD(A; B) = hS; ; !; fAg; fBgi de ned as follows: the set of states S consists of the unary predicates in D; the alphabet is the set of binary predicates in D plus the special symbol >; the (unique) initial and nal states are A and B respectively; nally, the transition relation ! consists of the following transitions: { C !> D for each E L-rule C(x) ! D(x) in D; { C !R D for each E L-rule R(x; y) ^ C(y) ! D(x) in D.
Finally, we denote with L(AutD(A; B)) the language accepted by AutD(A; B). Example 4.9 The automaton for D2 relative to hA; Bi is given below: start
A
B R R The automata for hA; Ai, hB; Ai, and hB; Bi contain exactly the same states and transitions and only di er on the particular choice of initial and nal state.
of some regular expression over the alphabet of the automaton. We adopt the following de nition of regular expressions over , where 2 and the atomic expression ; denotes the empty language.
e ::=
j ; j ee j e + e j e With each regular expression e over we uniquely associate a (fresh) binary predicate Ne and a Datalog program Pe that de nes Ne as shown next. De nition 4.10. Let D be a linear E LU -program and let e be a regular expression over the binary predicates in D and the symbol >. The Datalog program Pe corresponding to e is de ned inductively as follows:
P; = ; P> = f>(x) ! N>(x; x)g
PR = fR(x; y) ! NR(y; x)g Example 4.11 The language of the automaton AutD2 (A; B) in Example 4.9 can be captured by the regular expression ehA;Bi = R(RR) . The corresponding program PehA;Bi consists of the following Datalog rules:
R(x; y) ! NR(y; x) NR(x; y) ^ NR(y; z) ! NRR(x; z)
>(x) ! N(RR) (x; x) NRR(x; y) ^ N(RR) (y; z) ! N(RR) (x; z)
NR(x; y) ^ N(RR) (y; z) ! NR(RR) (x; z)
(
for each pair A; B in D n D_ we have that L(AutD(A; B)) can be described by some regular expression ehA;Bi, all ways in which an assertion A(a) can imply
the disjunctive program D0 de ned as the union of D_, all programs PhA;Bi, and all rules NehA;Bi (x; y) ^ A(x) ! B(y) has the same Horn consequences as
however, to ensure termination we do the following instead: Procedure 3 Rewrite-Datalog Input: D: a separable ELU -program; Output: P: a Datalog program 1: (D); (D) := ; 2: for each pair of unary predicates hA; Bi do 3: AutD(A; B) := nite word automaton for D relative to hA; Bi 4: Construct a regular expression ehA;Bi equivalent to AutD(A; B) 5: Construct Datalog program PehA;Bi and 6: (D) := (D) [ PehA;Bi 7: (D) := (D) [ fRehA;Bi ^ A(x) ! QB(y)g 8: P := Compile-Horn(D_ [ (D)) 9: P := P [ (D) 10: for each unary predicate A in D, replace QA with A in P 11: return P { in each rule NehA;Bi (x; y) ^ A(x) ! B(y) in D0, we replace predicate B with a fresh predicate QB, which ensures acyclicity of the resulting program; and { we apply Procedure 1 only to the monadic rules in D0, thus ignoring programs
The algorithm based on these ideas is given by Procedure 3. In Lines (
[ fNehA;Bi (x; y) ^ A(x) ! QB(y)g
In Line (
The following lemma shows that no Horn consequence is lost by applying
only afterwards.
Lemma 4.13. Let D be a separable E LU -program. Let P be the union of (D) and the output of Procedure 1 on D_ [ (D). Then, for every query A(x) and every ABox A, we have cert(A(x); D; A) = cert(QA(x); P; A).
Finally, in order to obtain a proper rewriting, in Line (
Theorem 4.14. On input a separable E LU -program D, Procedure 3 returns a Datalog rewriting of D.
Example 4.15 For our example program D2, we have the following: (D2) =
[
PehA;Bi = PR(RR) = f(
NR(RR) (x; y) ^ B(x) ! QA(y); N(RR) (x; y) ^ A(x) ! QA(y);
N(RR) (x; y) ^ B(x) ! QB(y)g 2 When applied to D_ [ Datalog rules:
(D2), Procedure 1 computes the following additional
NR(RR) (x; y) ^ N(RR) (x; y) ! QA(y)
NR(RR) (x; y) ^ N(RR) (x; y) ! QB(y)
(
In this paper, we have presented two su cient conditions for FO and Datalog rewritability of instance queries w.r.t. E LU -ontologies. Our results are still rather preliminary, and we are currently working on extending them in several ways.
First, we are con dent that our su cient conditions can be extended to cover also non-linear E LU -programs, as well as more expressive DLs such as ALCHI. Devising a resolution-based rewriting algorithm in such extended setting becomes, however, a much more challenging task.
Example 5.1 Consider the nonlinear E LU -program D3 with the following rules: >(x) ! A(x) _ B(x) D(x) ! H1(x) _ H2(x)
R(x; y) ^ A(y) ! D(x) D(x) ^ E(x) ! H(x)
B(x) ! A(x) D(x) ! E(x) This program is FO-rewritable: the non-linear rule D(x) ^ E(x) ! H(x) can be replaced with D(x) ! H(x) to obtain an equivalent linear program that satis es our su cient condition in Section 4.1. Procedure 1, however, does not terminate when given D3 as input; in particular, Procedure 1 will compute the following in nite family of disjunctive rules for each n > 1: " n # ^ R(yk; xk) ^ R(yk 1; xk) ^ D(yn) ! k=1 " n # _ H(yk) _ H1(y0) _ H2(y0) k=1 Second, it would be interesting to devise a resolution-based decision procedure for FO and Datalog rewritability for ALC ontologies; this is possible, since decidability has been recently shown. Finally, we are planning to implement our resolution algorithms and test them in practice.
in D. We call (D) the signature of D. If D is an E LU -program, we partition (D) into c(D), the set of all unary predicates (concept names) in D, and r(D), the set of all binary predicates (role names) in D.
lution, CloF (D) for the set of all rules derivable from D by positive factoring, and CloRF (D) for the set of all rules derivable from D by binary resolution and positive factoring.
Let x be a sequence of variables and let ' be a formula. We write xjzy and 'jzy for the result of substituting y for z in x and ', respectively. We write FV(') for the set of variables that occur free in '. Since we only consider formulas that are conjunctions or disjunctions of atoms, we can also view them as sets of atoms, writing A 2 ' for \A occurs in '". The notation A 2 r for a rule r is de ned analogously.
Proposition A.1. Let D be a linear E LU -program. Every rule in CloR(D) has the form A(x0) ^ ' ! Win=1 Bi(xi) where ' is a conjunction of binary atoms such that fx0; : : : ; xng FV(').
of binary atoms such that fx0; : : : ; xng Win=1 Bi(xi), where ' is a conjunction
FV('), we de ne:
Gr := (FV('); f (x; y) j 9R : R(y; x) 2 ' g) We call r tree-shaped if the following conditions are satis ed: 1. Gr is a tree with x0 as its root and x1; : : : ; xn as its leaves. 2. If fR1(x; y); R2(x; y)g ', then R1 = R2.
The depth of r is de ned as the depth of Gr.
Lemma A.2. Let D be a linear E LU -program. Every rule in CloR(D) is treeshaped.
Proof. By induction on the derivation of r 2 CloR(D). Clearly, all rules in D are tree-shaped. So, w.l.o.g., let r be a resolvent or r1 = A(x) ^ '1 ! Wim=1 Bi(xi) and r2 = B1(y) ^ '2 ! Win=1 Ci(yi) on B1(x1) and B1(y), respectively. By the inductive hypothesis, r1 and r2 are tree-shaped. Since FV('1) and FV('2) are assumed to be disjoint and the tree corresponding to r2 is rooted at y, the graph (FV('1 ^ ('2jyx1 )); f (x; y) j 9R : R(y; x) 2 '1 ^ ('2jyx1 ) g) is a tree rooted at x that has x2; : : : ; xm; y1; : : : ; yn; as its leaves. Moreover, since y has no incoming edge in Gr2 , we have R(x1; z) 2 '1 ^ ('2jyx1 ) if and only if R(x1; z) 2 '1 (for every variable z). The claim follows. tu Lemma A.3. Let D be a linear, acyclic E LU -program and let n be the maximal transfer depth of a unary predicate in D. Then each rule in CloR(D) has depth at most n.
Proof. Let r = A(x) ^ ' ! Win=1 Bi(xi) 2 CloR(D) By Lemma A.2, it su ces to show that, for every i 2 [1; n], the length of the (unique) path from x to xi in Gr is equal to the di erence between the transfer depth of A and the transfer depth of Bi. This follows by a straightforward induction on the derivation of r from D. tu De nition A.4 (n-Simulation). Let r = A(x0) ^ ' ! be a tree-shaped rule. We de ne an inductive family of preorders ( rn)n2N between variables in r as follows: x
r0 y :, f B j B(x) 2 x n+1 y :, r x
f B j B(y) 2 g g r0 y and for every R and x0 such that R(x0; x) 2 ' there is some y0 such that R(y0; y) 2 ' and x0 rn y0 We say x is n-simulated by y in r if x y and y rn x g. rn y. We de ne [x]rn := f y j x n r Lemma A.5. Let r be a tree-shaped rule of depth m and let x; y; z be variables such that, for some R, R(x; z); R(y; z) 2 r and x rn y for some n m. There is a substitution such that x = y, r is tree-shaped, and r r. Proof. The claim follows if we can show that for every tree-shaped rule r of depth m and every pair x; y such that x rm y, there is a substitution such that x = y and for every pair u; v of variables in the subtree of Gr rooted at x we have: 1. u ; v are variables in the subtree of Gr rooted at y. 2. For every variable u not in the subtree of Gr rooted at x: u
= u.
We prove the claim by induction on m. If m = 0, x and y have no successors
in Gr. Therefore, it su ces to show (
Now suppose m > 0. Let R1; : : : ; Rn, x1; : : : ; xn be all the predicate symbols
and variables such that Ri(xi; x) 2 r (i 2 [1; n]). Since x rm y, there are
y1; : : : ; yn such that Ri(yi; y) 2 r and x rm 1 y. By the inductive hypothesis,
there are substitutions 1; : : : ; n such that, for every i 2 [1; n]: xi i = yi and
i satis es (
Note that is well-de ned since the subtrees rooted at x1; : : : ; xn are pairwise
disjoint and do not contain x (which, in turn, holds since r is tree-shaped).
Clearly, satis es (
f (0) := 2j c(D)j f (n + 1) := 2j c(D)j j r(D)j 2f(n) Then [x]rn f (n) for every rule r over
(D) and every variable x in r.
A rule r is condensed if r has no condensation that is smaller than r. By Proposition A.6 and Lemma A.5 we obtain: Lemma A.7. Let D be an E LU -program. The size of condensed tree-shaped rules of depth n over (D) is bounded in n and j (D)j.
It su ces to show that the number of variables in every condensed tree-shaped rule of depth n is bounded by n (j r(D)j f (n))n.
Note that every tree T of depth n contains at most n mn nodes, where m is the maximal outdegree of a node in T . Therefore, every tree of depth n that has k nodes must contain a node that has outdegree at least pnk=n.
Suppose, for contradiction, r is a condensed tree-shaped rule of depth n that mentions more than n (j r(D)j f (n))n variables. By the above observation, Gr must have a node z that has outdegree greater j r(D)j f (n). Consequently, by Proposition A.6, there is some predicate R and two distinct variables x; y such that R(x; z); R(y; z) 2 r and [x]rn = [y]rn. By Lemma A.5, there is a substitution such that x = y and r r. Since x and y are distinct, it follows that r ( r, contradicting the assumption that r is condensed. tu Lemma A.8. Every condensation of a tree-shaped rule is tree-shaped. Proof. Let r be a tree-shaped rule and r a condensation of r. Since r is a subclause of r, Gr must be a forest, the root of Gr must be a source in Gr , and all leaves of Gr must be sinks in Gr . Since r is a substitution instance of r and Gr is connected, so must be Gr . Hence, Gr is a tree. The claim follows. tu Lemma A.9. Unrestricted binary resolution with condensation terminates on linear, acyclic E LU -programs. Moreover, the size of every rule derivable by binary resolution with condensation from an acyclic E LU -program D is bounded in the size of D.
Lemma A.8, every rule derivable by resolution with condensation is tree-shaped. By Lemma A.3 and Lemma A.7, the size and hence the number of condensed tree-shaped rules is bounded in j (D)j. The claims follow. tu Lemma A.10 ([8] Theorem 12, Lemma 19). Let D be a disjunctive program, let A be an ABox, and let C be a Horn clause such that D [ A j= C. Let DHi be the Datalog program computed by Procedure 1 after i iterations of the main loop. Then there is some n such that DHn [ A j= C.
Theorem A.11. Let D be a linear, acyclic E LU -program. Procedure 1 terminates on D and returns a Datalog rewriting of D.
Proof. To show termination of Procedure 1, it su ces to bound the size of every rule derived from D by resolution with condensation and factoring. By Lemma A.9, the size of every rule derived from D by resolution with condensation but no factoring is bounded in j (D)j. Thus, it su ces to show that for every rule r obtained from D by resolution with condensation and factoring there is a (not necessarily strictly) larger rule r0 obtained from D by resolution with condensation but without factoring such that r is subsumed by r0 (where clauses are viewed as sets of atoms). This follows by a straightforward induction on the derivation of r.
Let D be a linear, acyclic E LU -program and let r = A(x) ^ ' ! Win=1 Bi(xi) 2
to xi in Gr is equal to the di erence between the transfer depth of A and the transfer depth of Bi. In particular, if Bi = Bj for some 1 i < j n, then xi and j must have the same distance from x in Gr. Thus, while factoring can destroy the tree structure of Gr, it does not change the distance between x and xi in Gr. The same is true for condensation. Thus, we have: Proposition A.12. Let D be a linear, acyclic E LU -program, let PWbin=e1aBDi(axtai)lo2g rewriting of D computed by Procedure 1, and let r = A(x) ^ ' ! P. Then for every i 2 [1; n], the distance between x and xi in Gr is equal to the di erence between the transfer depth of A and the transfer depth of Bi.
depth of Gr is still bounded by the maximal transfer depth of a predicate in D and cannot be further increased by resolution.
Theorem 4.4. Given an acyclic E LU -program D and a unary predicate A in D, Procedure 2 terminates and returns a UCQ rewriting of A(x) w.r.t. D. Proof. By Theorem A.11, the call to Procedure 1 (Compile-Horn) terminates and returns a Datalog rewriting of D. It is easily seen that the main loop of the procedure computes the A-expansions of D as de ned in [7] (similarly to the algorithm in [14]). Therefore, the procedure terminates and returns a UCQrewriting of A(x) w.r.t. D provided the resolution strategy implemented in the main loop terminates.
Suppose, for contradiction, this is not the case. Then for every n 2 N, P00 must eventually contain a rule r such that Gr contains more than n nodes and r is not subsumed by any clause previously added to P00. By Proposition A.12, the depth of every rule in CloR(P [ fA(x) ! Q(x)g) is bounded in D. So, let d be the corresponding bound. It follows that Gr must contain a variable x with outdegree at least pdn=d. For large enough n, this means there is a rule r 2 P and rules r1 = B(y) ^ '1 ! Q(x), r2 = B(y) ^ '2 ! Q(x) 2 P0, r10, r20 such that r10 is a resolvent of r with r1, r2 is derived from r10 (and hence '1 '2), and r20 is a resolvent of r with r2. It is easily seen that r10 subsumes r0 . Moreover, 2 since r20 is derived from r10, r10 is added to P00 before r20, in contradiction to our assumption. tu B
Lemma 4.12. Let D be a linear E LU -program that is separable. Then, Procedure 1 terminates on D_ [ (D).
acyclic and every rule added by
(D) is acyclic, which is the case since D_ is (D) leads to a sink. tu
For the proof of Lemma 4.13, we need to generalise the notion of annotations from how they are de ned in x4.2. Let x, y, z be nite sequences of variables. Annotations are now triples of the form (x; S; y), where S is a set of binary atoms whose free variables are contained in x; y; z. Let = (x; S; y) be an annotation and let A = A1; : : : ; Ajxj, and B = B1; : : : ; Bjyj be nite sequences of unary predicates. We de ne the following notation for disjunctive rules: 0 jxj 1 A B := 8xyz: @ ^ Ai(xi)A ^ i=1 ^ C C2S !
jyj ! _ Bj (yj ) j=1 For linear rules, the notation reduces to A B, while for Datalog rules, we have
be of the form (x; fR(y; x)g; y) or (x; ;; x : : : x) for some n 1.
| {nz }
Let = (x; S; y), = (x0; S0; y0) be annotations such that FV( ) \ FV( ) = ;, and let i 2 [1; jyj], j 2 [1; jx0j]. We de ne: i j
:= (xx01 : : : x0j 1x0j+1 : : : x0jx0j; S [ (S0jyxi0j ); y1 : : : yi 1yi+1 : : : yjyj(y0jyxi0j )) We call 1 j as i j j , the composition of at position i to i1 as i , and 11 as at position j. We abbreviate .
Proposition B.1. Let = (x ; S ; y ); = (x ; S ; y ); = (x ; S ; y ) be annotations and let i; i0 2 [1; jy j], j 2 [1; jx j], k 2 [1; jy j], l 2 [1; jx j]. Then: 1. ij ( lk ) = ( 2. If i < i0, then (
ij ) lk+jy j 1 . ij ) li0 1 a ( i0 ) ij .
l
Let r = A B, r0 = A0 0B0 be two rules such that Bi = A0j and FV( ) \ FV( ) = ;. We write r +ij r0 for the resolvent of r and r0 on Bi(yi) and A0j (x0j ), respectively. We abbreviate r +j1 r0 as r +j r0, r +i1 r0 as r +i r0, and r +11 r0 as r + r0. Resolution naturally corresponds to composition of annotations: Proposition B.2. Let r = A B, r0 = A0 0B0 be linear rules such that Bi = A0 and FV( ) \ FV( 0) = ;. Then: 1. r +i r0 = A( i 0)B1 : : : Bi 1Bi+1 : : : BjBjB0. 2. If r is Datalog, then r + r0 = A( 0)B0.
We consider two rules r, r0 to be the same (and write r = r0) if they are identical up to renaming of bound variables and reordering of literals. The corresponding equivalence on annotations can be de ned as the least equivalence relation a such that: 1. (x1 : : : xm; S; y1 : : : yn)
for all 1 2. (x; S; y) a (x1 : : : xi 1xj xi+1 : : : xj 1xixj+1 : : : xm; S;
y1 : : : yk 1ylyk+1 : : : yl 1ykyl+1 : : : yn) i j m and 1 k l n, a (xjvu; Sjvu; yjvu) for every u 2= x [ y [ FV(S).
Proposition B.3. Two rules of the form A B, A B are identical up to renaming of bound variables and reordering of literals if and only if a .
We assume ij and +ij to be left-associative, writing r1 +ij11 r2 +ij22 r3 for (r1 +ij11 r2) +ij22 r3 and 1 ij11 2 ij22 3 for ( 1 ij11 2) ij22 3. As corollaries of Proposition B.1, we obtain: Corollary B.4. Let r = A B, r0, r00 be linear rules and i; j indices such that r +i (r0 +j r00) is a resolvent of r, r0 and r00. Then: 1. r +i (r0 +j r00) = r +i r0 +j+jBj 1 r00. 2. If r is Datalog, then r + (r0 +j r00) = r + r0 +j r00.
Corollary B.5. Let r = A B; r0; r00 be linear rules and i; j indices such that i < j and r +j r00 +i r0 is a resolvent of r, r0, and r00. Then r +i r0 +j 1 r00 = r +j r00 +i r0.
Lemma B.6. Let D be a separable E LU -program, let P be a Datalog program such that (P) \ c(D) = ; and no rule in P resolves with a rule in D_, and let r 2 CloR(D [ P) be linear. Then either r 2 CloR(D_ [ P) or, for some n 0, we have r = r_ + r1 + : : : + rn where: { r_ = A B 2 CloR(D_) where jBj { fr1; : : : ; rng CloR(D_ [ P). 1. r00 2 CloR(D_ [P). Then either i 2 [m+1; n] or i 2 [1; m]. In the former case, the claim is immediate. In the latter case, the claim follows by Corollary B.4. 2. r00 2 CloR(D [ P) n CloR(D_ [ P). Then r00 = r_00 + r100 + : : : + rk00 where r_00 = A00 00B00 2 CloR(D_) and fr100; : : : ; rk00g CloR(D_ [ P). Moreover, n = m + k an jBj = jB0j + jB00j. Since no unary predicate in D_ occurs in the body of a rule in D_, we have i 2 [m + 1; n]. W.l.o.g., let i = 1 (we can always achieve this by reordering the literals in r00). Then r = r_0 + r10 + : : : + rm0 + (r_00 + r100 + : : : + r00) k = r_0 + r10 + : : : + rm0 + r_00 +jB0j r100 +jB0j : : : +jB0j rk00 = (r_0 +m+1 r00 ) + r10 + : : : + rm0 +jB0j r100 +jB0j : : : +jB0j rk00
_ by Corollary B.4 and Corollary B.5. Therefore, we have r = r_ + r10 + : : : + rm0 + r100 + : : : + rk00 where r_ is obtained from r_0 +m+1 r_00 by moving the last jB00j literals right after the rst m literals. tu
transition system (i.e., automaton without initial and nal states). Every rule
a natural notion of a path between two unary predicates in P as a sequence of \connected" rules.
Proposition B.7. Let P be a linear E L-program and let r be a rule. Then r 2 CloR(P) i there is a path r1; : : : ; rn (n 1) in P such that r = r1 + : : :+ rn. Corollary B.8. Let P be a linear E L-program and let r = A B be a rule where A 6= B. Then r 2 CloR(P) if and only if there is a word 1 : : : n 2 L(AutP (A; B)) such that = 1 : : : n.
Given an annotation = (u; S; v) and variables x; y 2= FV(S), we write (x; y) for the formula VC2S (Cjxuyv). If S is empty, the notation is only de ned if x = y and stands for >(x).
P; P = ; = f (x; y) ! N (x; y)g
Pe1e2 = Pe1 [ Pe2 [ fNe1 (x; y) ^ Ne2 (y; z) ! Ne1e2 (x; z)g Pe1+e2 = Pe1 [ Pe2 [ fNe1 (x; y) ! Ne1+e2 (x; y); Ne2 (x; y) ! Ne1+e2 (x; y)g Pe
= Pe [ f>(x) ! Ne (x; x); Ne(x; y) ^ Ne (y; z) ! Ne (x; z)g Proposition B.9. Let P be a linear E L-program, let e be a regular expression over annotations in P, and let L(e) be the language represented by e. Then for every sequence 1; : : : ; n (n 1) of annotations in P: 1 : : : n 2 L(e) i n)(x; y) ! Ne(x; y) 2 CloR(Pe) Proposition B.10. Let P be a linear E L-program and let e1; : : : ; en be regular expressions over rule annotations in P. Then Pe1 [ [ Pen is a conservative extension of Pe1 in the sense that for every conjunction of atoms ': ' ! Ne1 (x; y) 2 CloR(Pe1 ) i ' ! Ne1 (x; y) 2 CloR(Pe1 [
Given a disjunctive program D, we write CloSR(D), CloSF (D), and CloSRF (D) for the set of all rules subsumed in CloR(D), CloF (D), and CloRF (D), respectively. Lemma B.11. Let D be an E LU -program such that CloR(D) = D and let R be a Datalog program such that c(D) \ (R) = ;. Then:
CloSR(D [ R) = CloSR(R) [ ^ ' !
^ '0 ! is subsumed in D; ' ! '0 2 CloSR(R) where denotes conjunctions of unary atoms, denotes disjunctions of unary atoms, and '; '0 denote conjunctions of binary atoms.
Proof. The inclusion from left to right is immediate. For the other inclusion, suppose r = ^ ' ! 2 CloR(D [ R) n CloR(R). We show the existence of a rule ^ '0 ! 2 D such that ' ! '0 2 CloSR(R) by induction on the derivation of r 2 CloR(D [ R). If r 2 D, the claim is immediate, so suppose r is obtained by resolution from r1; r2 2 CloR(D [ R). Since r 2= CloR(R), fr1; r2g 6 CloR(R). We prove the claim for fr1; r2g \ CloR(R) = ; (the other case is similar but simpler). Let r1 = 1 ^ '1 ! 1 and r2 = 2 ^ '2 ! 2. Since r is a resolvent of r1 and r2, we have ' = '1 ^ '2. By the inductive hypothesis, there are rules r10 = 1 ^ '01 ! 1 and r20 = 2 ^ '02 ! 2 such that '1 ! '01 2 CloSR(R) and '2 ! '02 2 CloSR(R). Then r0 = ^ '01 ^ '02 ! is a resolvent of r10 and r20 and hence r0 is subsumed by a clause in D. Since '1 ! '01 2 CloSR(R) and '2 ! '02 2 CloSR(R), we have '1 ^ '2 ! '01 ^ '02 2 CloSR(R). The claim follows. Similarly, we have: Lemma B.12. Let D be an E LU -program such that CloRF (D) = D and let R be a Datalog program such that c(D) \ (R) = ;. Then: tu CloSRF (D [ R) = CloSR(R) [ ^ ' !
^ '0 ! is subsumed in D; ' ! '0 2 CloSR(R) Proof. Proceeds analogously to the proof of Lemma B.11 with the additional observation that CloR(R) = CloRF (R) since R is a Datalog program. tu
Lemma B.13. Let D be an E LU -program, let R be a Datalog program such that c(D) \ (R) = ;, and let r be a Datalog rule. Then: r 2 CloSRF (D [ R) i
r 2 CloSR(CloRF (D)H [ R)
CloRF (D[R) CloRF (CloRF (D)[R). Therefore, by Lemma B.12, r 2 CloSR(R)[ f ^ ' ! j ^ '0 ! 2 CloSRF (D); ' ! '0 2 CloSR(R) g. On the other hand, since CloRF (CloRF (D)H ) = CloRF (D)H , we have CloSR(CloRF (D)H [ R) = CloSR(R) [ f ^ ' ! j ^ '0 ! 2 CloSRF (D)H ; ' ! '0 2 CloSR(R) g. The claim follows since r is Datalog. tu Lemma B.14. Let P be a linear E L-program, let r = A B be a rule where A 6= B, and let A 2 S c(P). Then: r 2 CloSR(P) i
r 2 CloSR(fA(x) ^ NehA;Bi (x; y) ! B(y)g [ PehA;Bi ) A B 2 CloSR(P) , r00 2 CloSR(PehA;Bi )).
Proof. Let r0 = A(x) ^ NehA;Bi (x; y) ! B(y). For the direction from left to right, suppose r 2 CloR(P). By Corollary B.8 and Proposition B.9, r00 = (x; y) !
CloRF (fr0g) = fr0g and (PehA;Bi ) \ fA; Bg = ;, we have r 2 f A(x) ^ ' ! B(y) j ' ! NehA;Bi (x; y) 2 CloSR(PehA;Bi ) g (by Lemma B.12), and thus r00 2 CloSR(PehA;Bi ). The claim follows by Proposition B.9 and Corollary B.8 (it is easily seen that the equivalence A B 2 CloR(P) , r00 2 CloR(PehA;Bi ) implies tu
and r30 a resolvent of r10 and r2. Then there is a rule r3 such that:
Lemma B.16. For every linear E LU -program D: CloSRF (D) = CloSF (CloR(D)).
Lemma B.17. Let D be a linear E LU -program and let R be a Datalog program such that c(D) \ (R) = ;. Then CloSRF (D [ R) = CloSF (CloR(D [ R)). Proof. Clearly, CloF (CloR(D [ R)) CloRF (D [ R). So, let r 2 CloRF (D [ R) = CloRF (CloRF (D) [ R) CloSR(R) [ f ^ ' ! j ^ '0 ! 2 CloSRF (D); ' ! '0 2 CloSR(R) g (by Lemma B.12). By Lemma B.16, r 2 CloSR(R) [ f ^ ' ! j ^ '0 ! 2 CloSF (CloR(D)); ' ! '0 2 CloSR(R) g = CloSF (CloR(R) [ f ^ ' j ^ '0 ! 2 CloR(D); ' ! '0 2 CloR(R) g). The claim, r 2 CloSF (!CloR(D [ R)), follows by Lemma B.11. tu Lemma B.18. Let D be a separable E LU -program. Let, for every A 2 c(D), QA be the predicate introduced for A in (D). Let D0 = D [ SA02 c(D)fA0(x) ! QA0 (x)g and let r = A QB be a rule where A; B 2 c(D). Then: r 2 CloSRF (D0) i r 2 CloSR(CloRF (D_ [
such that r 2 CloSF (fr0g). By Lemma B.6, either r0 2 CloR(D_0) or r0 = r_ + r1 + : : : + rn where r_ 2 CloR(D_0) and r = Aa iQB 2 CloR(D_0) (i 2 [1; n]). We show the claim for the second case as the rst case is similar but simpler. By Lemma B.14, we have ri 2 CloSR(fAi(x) ^ NehAi;QBi (x; y) ! B(y)g [ PehAi;QBi ) CloSR(D_[ (D)[ (D)) (i 2 [1; n]). Therefore, r0 2 CloSR(D_[ (D)[ (D)) and, consequently, r 2 CloSRF (D_ [ (D) [ (D)). The claim follows by Lemma B.13.
then have r 2 CloSRF (D_ [ (D) [ (D)). By Lemma B.17, there is some r0 2 CloR(D_ [ (D) [ (D)) such that r 2 CloSF (fr0g). By Lemma B.6, either r0 2 CloR( (D) [ (D)) or r0 = r_ + r1 + : : : + rn such that r_ 2 CloR(D_) and fr1; : : : ; rng CloR( (D) [ (D)).
Let P0 = SA02 c(D)fA0(x) ! QA0 (x)g. It su ces to show that for every i 2 [1; n]: ri 2 CloSR(D_ [ P0) (since then r 2 CloSF (CloSR(D_ [ D_ [ P0)) = CloSRF (D0)). So, let i 2 [1; n] and let ri = Ai iQB. By de nition, no two rules in (D) resolve with each other. Moreover, the rules in (D) have pairwise distinct unary predicates in their bodies. Therefore, with Lemma B.11, we obtain ri 2 CloSR(fAi(x) ^ NehAi;QBi (x; y) ! QB(y)g [ (D)). The claim follows by
Proposition B.19. Let F be a set of FO-sentences and let r be a Datalog rule of the form ' ! H. Then F j= r if and only if for every substitution from the variables in r to individuals: F [ f' g j= H .
Lemma B.20. Let D be an E LU -program, let P be an E L-program, and let Q be a unary predicate such that (D) (P) and for every Datalog rule r = ' ! Q(x) over (D): r 2 CloSRF (D) i r 2 CloSR(P) Then for every ABox A over
(D) and every individual a: D [ A j= Q(a) i
P [ A j= Q(a) Proof. Suppose D [ A j= Q(a). Let be a substitution mapping each individual in A to a distinct variable and let r = (V A) ! Q(a ). By Proposition B.19, we then have D j= r. Then, by completeness of binary resolution with positive factoring, r 2 CloSRF (D), and hence r 2 CloSR(P) by the assumption. Since binary resolution with factoring is a sound inference calculus, we have P j= r, and hence D [ A j= Q(a) by Proposition B.19 (as the inverse of is a substitution from variables in r to individuals).
The other direction follows analogously since binary resolution without factoring is a sound and complete inference calculus for Horn clauses. tu Theorem 4.14. On input a separable ELU -program D, Procedure 3 returns a Datalog rewriting of D.
serve that, by Lemma 4.13, D [ A j= A(a) whenever P [ A j= QA(a). So, replacing QA by A in P does not allow to derive anything that is not entailed by the original program.