Resolution-based rewriting algorithms have been widely used for computing disjunctive datalog rewritings for DL TBoxes, and recently, also for computing datalog rewriting for queries over TBoxes expressed in DL-Lite and ELHI. Although such algorithms are general enough to support a wide variety of (even very complex) DLs, this generality comes with performance prices. In the current paper we present a resolution-based (query) rewriting algorithm for ELHI that is based on a hyper-resolution like inference rule and which avoids performing many redundant inferences. We have implemented the algorithm and have conducted an experimental evaluation using large and complex ontologies.
is then saturated using resolution to derive new (datalog) clauses. On the one hand, such calculi are worst-case optimal and allow for a large number of existing optimisations, like ordering restrictions and subsumption deletion. On the other hand, since there exist many resolution-based decision procedures for expressive fragments of rst order logic [9, 13] it is (relatively) easier to design a resolutionbased rewriting algorithm for an expressive DL compared to designing a custom made one. For example, to the best of our knowledge, none of the tailor made systems for DL-Lite can currently support more expressive DLs.
However, the e ciency of resolution-based approaches has also been criticised [22]. Even with all existing optimisations the saturation can perform many redundant inferences producing clauses that contain function symbols and which don't subsequently lead to the generation of function-free (datalog) clauses that are part of the rewriting. Hence, tailor made approaches have greatly surpassed the resolution-based ones [22, 14]. To circumvent this issue and provide an e cient resolution-based query rewriting algorithm for DL-Lite, an optimised hyperresolution like inference that avoids producing (intermediate) redundant clauses that contain function symbols has been proposed [7]. The calculus was implemented in Rapid and as shown also by independent evaluations, Rapid is currently one of the fastest query rewriting systems [7, 14], however, like most of them it can only support DL-Lite.
In the current paper we investigate whether a resolution-based rewriting algorithm that is based on a similar hyper-resolution step can be de ned for for E LHI TBoxes. This is a technically very challenging task as the structure of E LHI axioms implies many complex interactions between the clauses (in contrast to DL-Lite, E LHI is not FO-rewritable and subsumption checking is in ExpTime). However, we show that a rewriting can be computed by a calculus that contains an extension of the hyper-resolution step of DL-Lite plus a new resolution rule that we expect to be rarely applied in practice. To achieve this we rst cast the Rapid calculus for DL-Lite to the framework of resolution and sketch its correctness. Finally, we conducted an experimental evaluation using large-scale real-world ontologies. Our results show that in many tests state-ofthe-art systems cannot compute a rewriting within a reasonable amount of time (more than one hour) compared to the new implementation. 2
We use the standard notions of rst-order term, atom, variable, sentence, constant, function symbols, functional terms, entailment (j=), and the like. Resolution-Based Calculi We use standard notions from (resolution) theoremproving like clause, (hyper-)resolvent and most general uni er (mgu). An inference rule, or simply inference is an n + 1-ary relation usually written as follows:
C where C1 is called the main premise, C2; : : : Cn are called the side premises and C is called the conclusion or resolvent. An inference system I, also called calculus, C1
C2 : : : Cn is a collection of inference rules. Let be a set of clauses, C a clause and I an inference system. A derivation of C from by I, written `I C (or simply ` C if I is clear from the context), is a sequence of clauses C1; : : : ; Cm such that Cm = C, each Ci is either a member of or the conclusion of an inference by I from [ fC1; : : : ; Ci 1g. In that case we say that C is derivable from by I. We write `i C to denote that the depth of the corresponding derivation tree [6] constructed for C from is less or equal to i. We also often write ; C ` C0 instead of [ fCg ` C0. An inference system with particular interest to us is SLD, denoted by ISLD, where all side premises are members of . Description Logics Let C, R, and I be countable, pairwise disjoint sets of atomic concepts, atomic roles, and individuals. An E LHI-role is either an atomic role P or its inverse P . The set of E LHI-concepts is de ned inductively as follows, where A 2 C, R is an E LHI-role, and C(i) are E LHI-concepts: C := > j ? j A j C1 u C2 j 9R:C An E LHI-TBox T is a nite set of GCIs C1 v C2, with Ci E LHI-concepts, and RIAs R1 v R2 with Ri E LHI-roles. We assume from now on that E LHI-TBoxes are normalised, i.e., they contain only GCIs of the form A1 v A2, A1 uA2 v A, A1 v 9R:A2, or 9R:A2 v A1, where A(i) 2 C[f>g, and R 2 R. An ABox A is a nite set of assertions A(a) or P (a; b), for A 2 C, P 2 R, and a; b 2 I. An E LHI-ontology is a set O = T [ A. DL-Lite is obtained from E LHI by disallowing GCIs of the form 9R:A1 v A2 where A1 6= >.1 We call such GCIs RA-GCIs while all the rest DL-Lite-GCIs.
Queries and Query Rewriting A datalog rule r is an expression of the form H B1 ^ : : : ^ Bn where H, called head, is a (possibly empty) function-free atom, fB1; : : : ; Bng, called body, is a set of function-free atoms, and each variable in the head also occurs in the body. A variable that appears twice in the body and not in the head is called ej-variable; we use ejvar(r) to denote all ej-variables of r. A datalog program P is a nite set of datalog rules. A union of conjunctive queries (UCQ) Q is a set of datalog rules such that their head atoms share the same predicate, called query predicate, which does not appear anywhere in the body. A conjunctive query (CQ) is a UCQ with exactly one rule. We often abuse notation and identify a CQ with the only rule it contains instead of a singleton set. For a query Q with query predicate Q, a tuple of constants ~a is an answer of Q w.r.t. a TBox T and an ABox A if the arity of ~a agrees with the arity of Q and T [ A [ Q j= Q(~a). We denote with cert(Q; T [ A) the answers to Q w.r.t. T [ A. Finally, we recall the notion of (query) rewriting [3, 19, 21]. De nition 1. Let Q be a CQ with query predicate Q and let T be a TBox. A datalog rewriting (or simply rewriting) R of a CQ Q w.r.t. T is a datalog program whose rules can be partitioned into two disjoint sets, RD and RQ such that RD does not mention Q, RQ is a UCQ with query predicate Q, and where 1 In the literature, this DL is called DL-LiteR;u [4], however, for simplicity we call it DL-Lite. Typically, DL-Lite also allows for axioms of the form A1 v :A2 and R1 v :R2, however, these do not have any e ects in query answering when T [ A is consistent (see, e.g., [19]); hence we will discard them here. for each A consistent w.r.t. T and using only predicates from T we have: cert(Q; T [ A) = cert(RQ; RD [ A): The Requiem System Throughout the paper we will use the inference system implemented by Requiem as a yardstick, to highlight the ine ciencies of typical resolution-based rewriting algorithms and sketch completeness of the re ned approach. Like most rewriting systems, the behaviour of Requiem on input Q and T can be characterised by the application of the following three steps: 1. Clausi cation: the input TBox T is transformed into a set of clauses TC, using standard techniques like skolemisation (see Example 1). 2. Saturation: TC [Q is saturated by using (binary) resolution with free selection sat.
[2] (denoted as IREQ) computing a new set TCsat are returned. 3. Post-processing : all function-free clauses in TC Next, we brie y illustrate the Requiem calculus through an example. Example 1. Consider the TBox T consisting of the following GCIs (left side), together with the respective clauses produced at step 1. (right side): A v 9R:B
R v S
R(x; f (x)) As can be seen, the rst GCI produces two clauses, where f is a skolem function that is uniquely associated with the speci c occurence of concept 9R:B.
Consider now the query Q1 = Q(x) S(x; y) ^ C(y). When applied to Q1
and T the Requiem algorithm would perform the following inferences:
(2a) and (
A(x)
Q1 and (
A(x) ^ C(f (x))
Finally, the function-free set returned is R = fQ1; (
Conventions To simplify the presentation, in the following we assume that TBoxes are given in a clausal form. Clauses that are produced by clausfying RAGCIs and DL-Lite-GCIs are called RA-clauses and DL-Lite-clauses, respectively. Finally, clauses with the query predicate in the head are called Q-clauses ; note that such clauses can contain functional terms in the body (e.g., clause Q2 in Example 1). 3
In the current section we present a hyper-resolution like rewriting algorithm
for DL-Lite, which characterises the algorithm implemented in Rapid using the
framework of resolution. In addition, we sketch its proof of correctness, which
implies correctness of Rapid; this is also important subsequently for E LHI.
Example 2. Consider the TBox T and query Q1 from Example 1 as well as the
inferences performed by IREQ on T [ Q1. As it can be observed the algorithm
performed two redundant inferences since neither clauses (
These clauses would be of importance only if a clause of the form C(x)
B(x) also existed in T . Then, the latter would resolve with (2b) producing
C(f (x)) A(x) which would subsequently resolve with Q2 to produce Q(x)
A(x), that would be part of R. }
As it has been argued in [22], TBoxes typically contain many clauses of the
form R(x; fi(x)) Ai(x). Together with clause (
One could try to remedy the above issue by applying the following
approach/re nement on IREQ: rst, saturate the clauses of T obtaining Tsat and
then, resolve Q1 with (
Our inability to e ciently implement the above re nement is because IREQ
follows a \forward" style approach to apply resolution which generates new
clauses that contain function symbols (e.g., clause (
Q Q
Q0
C
C1 C2 unfolding:
s.t. if x 7! f (y) 2 ; then x 62 ejvar(Q) shrinking:
Q0 Finally, for Q a CQ and T a DL-Lite-TBox let Rapid-Lite(Q; T ) be all functionfree clauses derivable from Q [ T by Ilite. Intuitively, unfolding corresponds to all classical binary resolution inferences that won't introduce function symbols in Q, while shrinking is a hyper-resolution step which \eliminates" an ej-variable of Q using clauses that mention a functional term f .
Example 3. Consider T and Q1 from Example 1 and consider also the TBox T 0 = fC(x) B(x)g [ T . Applying Ilite to T [ Q1 performs the following inferences:
unfolding on Q1 and (
B(x) produces Q03 = Q(x) shrinking on Q03; (2a); and (2b) produces Q4 = Q(x) R(x; y) ^ C(y) R(x; y) ^ B(y) A(x) The set R0 = fQ1; Q02; Q03; Q4g is a rewriting of Q1 w.r.t. T . } Correctness of our rewriting algorithm follows by showing how a derivation constructed by IREQ can be transformed into a derivation by Ilite; hence, saturating T [ Q by Ilite will create all necessary members of a rewriting. This is done in two steps. First, we show that each Requiem derivation can be transformed into an SLD derivation.
Lemma 1. Let T be a DL-Lite-TBox and let Q be a CQ with query predicate Q. Every Q-clause Q0 derivable from T [ Q by IREQ is also derivable from T [ Q by ISLD.
The Lemma is proven by showing how to \unfold" a Requiem inference Q; C ` Q0 where T `i C into Q; C1 ` Q00; Q00; C2 ` Q0 where T `i 1 C1; T `i 1 C2 and C1; C2 ` C. By repeated application of this unfolding we will eventually (fully) unfold any derivation of a Q-clause Q0 into inferences of the form Q; C1 ` Q1; : : : ; Qn 1; Cn ` Q0, where Ci 2 T , i.e., into an SLD derivation of Q0.
Second, we show that each SLD derivation can be transformed into a derivation by Ilite. By de nition of Ilite and Example 3 we can see that inferences using the unfolding rule directly corresponds to one SLD inference, while shrinking corresponds to many SLD inferences where, the main premise is a function-free CQ, the side premises contain the same function symbol f , and the conclusion is also a function-free CQ. Hence, we need to show that each SLD derivation can be transformed into one that satis es the following property.
De nition 3. Let Q1; Q2; : : : ; Qn be an SLD derivation of Qn such that Qi; Ci ` Qi+1 for some clause Ci. Assume also that all Q2; : : : ; Qn 1 contain a term that mentions a function symbol f while Q1 and Qn are function-free. We say that the derivation is function compact if all side premises Ci with 1 i < n used in the derivation also mention f .
The following can be shown for Horn clauses with one existential variable. Lemma 2. Any SLD derivation can be transformed to a function compact one.
Using Lemmas 1 and 2 we can show the following.
Theorem 1. Let a DL-Lite-TBox T and a CQ Q. Every derivation from T [ Q by Ilite terminates. Moreover, Rapid-Lite(Q; T ) is a rewriting of Q w.r.t. T .
A Rewriting Algorithm for E LHI In the current section we extend the inference system Ilite in order to provide a (query) rewriting algorithm for E LHI ontologies.
E LHI additionally allows for RA-clauses of the form E(x) R(x; y) ^ F (x).
According to the Requiem calculus this clause interacts with clause (
A straightforward approach to obtain an e cient calculus for E LHI
ontologies would be to extend De nition 2 to allow for arbitrary E LHI-clauses as side
premises in shrinking and unfolding. Then, Lemmas 1 and 2 apply with few
modi cations and hence this calculus would produce a rewriting.
Example 4. Let T be the E LHI-TBox consisting of the following clauses:
(
B(x) ^ D(x) B(x) ^ C(f (x)) B(x) ^ D(x)
B(x) ^ D(x)
B(x) C(x) K(x)
S(x; y) ^ D(y)
S(y; x) ^ C(y) and let also the query Q1 = Q(x) K(x).
By unfolding on Q1 and (
Example 5. Consider the TBox T and query Q1 from Example 4. When applied
to T and Q1 the Requiem algorithm would perform the following inferences with
the respective conclusions:
(
function:
The set R = fQ1; (
First, we can observe that, if we extend shrinking to accept RA-clauses as
main premises, then the inferences performed to produce clause (
First, note that we had to extend shrinking to accept possibly more that two side
premises. This is because due to the function rule we can now deduce new clauses
that contain function symbols; hence there can be more than two clauses
containing some function f , unlike the case in DL-Lite. In practice, however, we expect
that n is small since such clauses are only produced by the function rule and
only when there is a complex interaction between a clause containing R(x; f (x))
(R(f (x); x)) and an RA-clause containing the inverse R(y; x) (R(x; y)).
Example 6. Consider Example 5. The inference between clauses (
A(x)
Again by inspection of IREQ we can see that clauses of form (
Lemma 3. Let P be a set of DL-Lite-clauses and let 1 be an RA-clause. Consider also a derivation 1; : : : ; n by IREQ, such that i; Ci ` i+1 and Ci is derivable from P by IREQ. Assume also that n is of the form A(x) B(x) ^ [C(x)] while no i with i < n is of the same form as n. Then, n can be derived from P [ 1 by unfolding and n-shrinking.
Using Lemma 3 and our observation regarding clauses of form (
Lemma 4. Let T be an ELHI-TBox and let Q be a CQ with query predicate Q. Let also Plt be all DL-Lite-clauses derivable from T by IEL. Then, every Q-clause Q0 derivable from T [ Q by IREQ is also derivable from Plt [ Q by ISLD.
Finally, we can show the following.
Theorem 2. Let an ELHI-TBox T and a CQ Q. Every derivation from T [ Q by IEL terminates. Moreover, Rapid-EL(Q; T ) is a datalog rewriting of Q; T . 5
We have extended the Rapid2 query rewriting system [7] to support ELHI ontologies. Rapid attempts to compactly represent many unfolding inferences as datalog rules in an e ort to compute small (datalog) rewritings.
We conducted an experimental evaluation comparing against Requiem [19], Presto [21], and Clipper [8], using real-world large scale DL-Lite and ELHI ontologies. Regarding DL-Lite, we used DL-Lite versions of the OpenGALEN2 (http://www.opengalen.org/), OBO protein (http://www.obofoundry.org/), and NCI 3.12e (http://evs.nci.nih.gov/ftp1/NCI_Thesaurus) ontologies, which we denote by Gd, Pd, and N, respectively. This part extends the evaluation in [7] for large scale ontologies, and uses datalog rewritings instead of UCQs. 2 http://www.image.ece.ntua.gr/~achort/rapid.zip Regarding E LHI, we used E LHI versions of the NASA SWEET 2.3 (http: //sweet.jpl.nasa.gov/ontology/), periodic table (http://www.cs.man.ac. uk/~stevensr/ontology/), OpenGALEN2, and OBO protein ontologies, which we denote by S, C, Ge, and Pe, respectively. The DL-Lite and E LHI versions of the ontologies where obtained by normalizing the ontologies and keeping the appropriate subset of axioms. Table 1 provides statistics for the ontologies. For each of them we manually constructed 5 test queries. All tests were performed on a dual core 1.8GHz Intel Celeron processor laptop running Windows 8 and JVM 1.7 with 3.6GB maximum heap size. The timeout limit was set to 2 hours.
The results for DL-Lite are shown in the upper part of Table 2, which includes the computation time and the size of the computed rewriting; \t=o" denotes timeout. First, we observe that neither Presto nor Clipper managed to compute a rewriting for Gd, Requiem required 9{18 minutes, while Rapid required only milliseconds. Similar observations can be made for the rest of the DL-Lite ontologies. Notable cases are queries 1{5 over N for Clipper, where it required about 13 minutes for each of them, query 5 over Pd and query 3 over N for Requiem, for which it did not manage to compute a rewriting, and all queries over Pd and N for Presto for which it required 1 to 2 hours, being in general much slower also from Requiem and Clipper. Rapid was slower only for query 5 over Pd, where it required 7:15 minutes. The analysis showed that 7:00 out of the 7:15 minutes are spent in backwards subsumption checking (which guarantees a compact result with no equivalent or subsumed queries), while the actual rewriting time is only 15 seconds. Note that no other system performs backwards subsumption. In fact, in this case e.g. Clipper returns several rewritings that are equivalent up to variable renaming, which justi es also the di erence in the rewriting sizes.
The results for E LHI are shown in the lower part of Table 2; we did not run Presto since it does not support E LHI. Our conclusions are similar to those of DL-Lite|that is, in the large scale ontologies Rapid greatly outperforms all other systems while in query 5 of the E LHI version of the OBO protein ontology (Pe) it performed worse than Clipper since it spent 13:27 out of the 13:52 minutes in backwards subsumption. Note also that for Ge, Rapid was the only system that managed to compute a rewriting within `reasonable' time (8{11 minutes).
In summary, we can see that computing even some rewriting over large scale and complex ontologies is still an unresolved issue as in many cases many stateof-the-art systems did not manage to terminate, required several minutes, or even hours. This could be acceptable if a rewriting is computed once for a xed ontology, however, practice has shown that ontologies are very often dynamic [5, 11, 10]. Moreover, in design time, ontology engineers tend to run reasoners often .08 .16 S .02 .05 .04 .06 .05 C .09 .08 .15 11:01.71 8:45.87 Ge 10:18.01 9:26.00 7:47.52 4.80 29.73 Pe 2.59
15.71 13:51.97 requiring more than a couple of minutes might not be acceptable. 6
We have presented an e cient resolution-based rewriting algorithm for E LHI . Despite the complex interactions in E LHI we show that a calculus using extensions of the unfolding and shrinking rules of Rapid for DL-Lite, plus a new rule can be de ned. Our experimental evaluation shows that there are large scale ontologies which existing systems cannot handle, while the new algorithm only requires milliseconds. This is to a large extent due to the hyper-resolution inference performed by shrinking, which avoids well-known ine ciencies of resolutionbased rewriting algorithms [22].
Concerning future work, we plan to investigate whether a similar hyperresolution step can be used to optimise resolution-based rewriting algorithms for non-Horn DLs like ALC, like those implemented in the KAON2 system [15].