We present an optimized query rewriting algorithm for OWL 2 QL that computes the rewriting set of a user query by avoiding unnecessary inferences and extended clause subsumption checks. The evaluation shows a significant performance improvement in comparison to other similar approaches. Alternatively, instead of a rewriting set, the algorithm can produce an equivalent non-recursive datalog program.
The problem of answering conjunctive queries (CQ) over expressive DL
ontologies suffers from high worst-case complexity. The DL-LiteR language [
Several CQ answering algorithms for DL-LiteR have been proposed. In [
In this paper we present Rapidf , a goal-oriented query rewriting algorithm
for queries posed over DL-LiteR ontologies. Instead of exhaustively performing
resolution, it performs a restricted sequence of inferences that lead directly to
rewriting sets with, hopefully, no unnecessary rewritings. In this way, we avoid
a large number of blind inference paths and the need for extended query
subsumption checks. Rapidf improves the Rapid algorithm [
A DL-LiteR ontology is a tuple ⟨T ; A⟩, where T is the terminology and A the assertional knowledge. Formally, T is a set of axioms of the form shown in Table 1, where A, B are atomic concepts and P , S atomic roles. A is a finite set of assertions of the form A(a) or P (a; b), where a; b are individuals.
A CQ Q has the form A ← B, where atom A is the head, and the set of atoms B (seen as a conjunction) is the body of Q. We denote B by body Q, and A by head Q. A CQ Q is posed over an ontology ⟨T ; A⟩ if the predicates of all atoms B ∈ body Q are entities of T and have arities 1 or 2, if the entity is a concept or a role, respectively. Hence, B is a concept atom B(t) or a role atom S(t; s). terms B (vars B, cons B) are the sets of terms (variables, constants) that appear in B. For a set of atoms B we have terms B = ∪B∈B terms B, for a CQ Q we have terms Q = terms ({head Q}∪body Q) and similarly for vars Q, cons Q. An atom or CQ is function free if it contains no functional terms. User queries are always function free. Given a function free CQ Q, a term t ∈ terms Q is called distinguished if it appears in head Q, and non distinguished otherwise; bound if it is a constant, or a distinguished variable, or a variable that appears at least twice in body Q, and unbound otherwise. We denote the set of bound terms, bound and unbound variables of Q by termsB Q, varsB Q and varsUB Q, respectively. For an atom A we also write varsB A and varsUB A instead of vars A ∩ varsB Q and vars A \ varsB Q, respectively, if it is clear that A ∈ body Q, for some Q.
A tuple of constants a is a certain answer of a CQ Q posed over the ontology
O = ⟨T ; A⟩ iff (O)∪{Q} |= C(a), where C is the predicate of head Q and (O)
the clausification of O into first order clauses (see Table 1, where it is assumed
that each axiom introduces a distinct function f ). The set that contains all
answers of Q over O is denoted by cert (Q; O). It has been proved [
Formally, a function free CQ Q′ is a rewriting of a CQ Q posed over ontology O, iff Q and Q′ have the same head predicate and (O)∪{Q} |= Q′. Nevertheless, not all possible rewritings are needed for the complete computation of cert (Q; O), since some of them may be equivalent or subsumed by others. We say that a CQ Q subsumes a CQ Q′ (or Q′ is subsumed by Q) and write Q ◃ Q′, iff there is a substitution such that head (Q ) = head Q′ and body (Q ) ⊆ body Q′. If Q and Q′ are mutually subsumed, they are equivalent. If Q is a set of CQs and for some CQ Q there is a Q′ ∈ Q equivalent to Q, we write Q ∈ˆ Q. A set rewr (Q; O) is a rewriting set of the CQ Q over O iff for each rewriting Q′ of Q over O, either Q′ ∈ˆ rewr (Q; O) or there is a Q′′ ∈ rewr (Q; O) such that Q′′ ◃ Q′. Given a CQ Q, let Q′ be the CQ head Q ← {B}B∈B for some B ⊆ body Q. If B is a minimal subset of body Q such that Q ◃ Q′, Q′ is called condensed or a condensation of Q, and is denoted by cond Q. Since a CQ is equivalent to its condensation, we can find cert (Q; O) by computing a rewriting set of Q that contains only condensed rewritings and no two rewritings Q; Q′ such that Q ◃ Q′. Hence, we say that Q′ is a core rewriting of a CQ Q over O, iff it is a rewriting of Q over O, it is condensed, and there is no (non equivalent) rewriting Q′′ of Q over O such that Q′′ ◃ Q′. The core rewriting set rewrC (Q; O) of Q over O is the set of all the core rewritings of Q over O.
Axiom A ⊑ B S ⊑ P S− ⊑ P ∃S ⊑ A A ⊑ ∃P A ⊑ ∃P:B ∃S ⊑ ∃P ∃S− ⊑ ∃P ∃S ⊑ ∃P:B ∃S− ⊑ ∃P:B
Clause B(x) ← A(x) P (x; y) ← S(x; y) P (x; y) ← S(y; x) A(x) ← S(x; y) P (x; f (x)) ← A(x) P (x; f (x)) ← A(x) B(f (x)) ← A(x) P (x; f (x)) ← S(x; y) P (x; f (x)) ← S(y; x) P (x; f (x)) ← S(x; y) B(f (x)) ← S(x; y) P (x; f (x)) ← S(y; x) B(f (x)) ← S(y; x)
Axiom S ⊑ P − S− ⊑ P − ∃S− ⊑ A A ⊑ ∃P − A ⊑ ∃P −:B ∃S ⊑ ∃P − ∃S− ⊑ ∃P − ∃S ⊑ ∃P −:B ∃S− ⊑ ∃P −:B
Clause P (y; x) ← S(x; y) P (y; x) ← S(y; x) A(x) ← S(y; x) P (f (x); x) ← A(x) P (f (x); x) ← A(x) B(f (x)) ← A(x) P (f (x); x) ← S(x; y) P (f (x); x) ← S(y; x) P (f (x); x) ← S(x; y) B(f (x)) ← S(x; y) P (f (x); x) ← S(y; x) B(f (x)) ← S(y; x) Rapidf computes rewrC (Q; O) for a user query Q in an efficient way. Its strategy is based on the distinguishing property of the bound variables, namely that whenever a CQ Q is used as the main premise in a resolution rule in which an atom A ∈ body Q unifies with the head of the side premise and the mgu contains a binding v=t for some variable v ∈ varsB Q, the application of affects several atoms of the query apart from A.
Rapidf consists of the following steps: (1) The clausification step, in which O is transformed into (O). (2) The shrinking step, in which the clauses of (O) are selectively used as side premises in resolution rule applications in order to compute rewritings which differ from the user query Q in that they do not contain one or more variables in varsB Q, because the application of the resolution rule led to their unification with a functional term which subsequently was eliminated. (3) The unfolding step, which uses the results of the previous step to compute the remaining rewritings of Q, by applying the resolution rule without that the bound variables of the main premise are affected. In principle, only unbound variables are eliminated or introduced at this step. However, some bound variables of the main premise may also be eliminated, not through the introduction and subsequent elimination of functional terms, but while condensing the conclusion. Obviously, the same can happen at the shrinking step. (4) The subsumption check step, in which subsumed rewritings are removed.
For efficienty, Rapidf does not implement the shrinking and unfolding steps by applying directly the resolution rule. Instead, a shrinking and unfolding inference rule are defined, which combine a series of several successful resolution rule application steps into one. In this way, the resolution rule is used only if it eventually leads to a function free and hopefully also non subsumed rewriting, and a large number of unnecessary inferences is avoided. The rules of Rapidf make use of the unfolding and function sets of atom. 3.1
(O) w.r.t. the resolution rule contains clauses of the form A(x) ← B(x); P (x; f (x)) ← B(x); P (g(x); f (g(x))) ← B(x); P (g(h(x)); f (g(h(x)))) ← B(x); : : :
A(x) ← S(x; y);
P (x; y) ← S(x; y); P (x; f (x)) ← S(x; y); P (g(x); f (g(x))) ← S(x; y); P (g(h(x)); f (g(h(x)))) ← S(x; y); : : : as well as the respective clauses with the role atom arguments inverted. We note that in the clauses of the first two rows, the non functional terms of the head appear also in the body. Based on this remark, and given that in the unfolding step we want the bound variables not to unify with functional terms but be preserved in the conclusion, we define the unfolding of an atom as follows: De nition 1. Let A be a function free atom and T a subset of terms A. Atom B ′ is an unfolding of A w.r.t. T iff (O) ⊢R A ← B for some substitution on a (possibly empty) subset of vars A \ T to functional terms, where ′ is a renaming of vars B \ T such that for v ∈ vars B \ T we have v ′ ∈= vars A.
In the above, ⊢R denotes derivability under the first-order resolution rule. Essentially, B ′ is an unfolding of A w.r.t. T if it is the body of a clause inferrable from (O) that has in its head an atom A′ (of the same predicate as A), and both B and A′ contain unaltered all terms in T (which should contain the bound terms in A). Since the variable renaming ′ contains no essential information, we collect all unfoldings and define the unfolding set of atom A for T w.r.t. (O) as the set D(A; T ) = {B | (O) ∪ {A} ⊢J (T ) B}, where J (T ) are the inference rules shown in Table. 2, in the form ABC . Given T , A (the main premise) and a clause C ∈ (O) (the side premise), by applying the respective rule we get atom B (the conclusion). We also define the set Dˆ(A; T ) = D(A; T ) ∪ {A}. It is easy to prove that given A and T ̸= ∅ we have (O) ⊢R A ← B iff B ′ ∈ D(A; T ), for ; ′ as defined in Def. 1.
rule A(t) A(f (x)) ← B(x)
B(z) A(t) A(f (x)) ← S(y; x)
S(w; z) A(t) A(x) ← S(y; x)
S(z; t) P (v; t) P (f (x); x) ← B(x)
B(t) P (v; t) P (f (x); x) ← S(x; y)
S(t; z) P (v; t) P (f (x); x) ← S(y; x)
S(z; t) P (t; s) P (x; y) ← S(y; x)
S(s; t) As we have already seen, the closure of (O) contains clauses of the form P (x; f (x)) ← B(x), P (f (x); x) ← B(x) and A(f (x)) ← B(x), as well as of the form P (g(x); f (g(x))) ← B(x) and P (g(x); f (g(x))) ← S(x; y). Unlike in the unfolding case, now we are interested in the behavior of the functional term f (x), which appears in the head but not in the body, because if f (x) appears in the body of a rewriting, it may be possible to eliminate it by using such clauses. Let funcs (O) be the set of all functions in (O). According to Table 1, each DL-LiteR axiom that has an existential quantifier in the RHS introduces a distinct function f . Hence, each function f ∈ funcs (O) is uniquely associated with the concept or role that appears in the LHS of the axiom that introduces f . Let atom f [x] denote the atom that (a) has as predicate the entity associated with f , (b) has the variable x in the place of the bound variable of the respective axiom of Table 1 which introduces f , and (c) has a distinct variable (not elsewhere used, as needed) in the place of the unbound variable, if any. E.g. if the axiom A ⊑ ∃P:B introduces function f1 then atom f1[x] is the atom A(x), and if the axiom ∃S− ⊑ ∃P:B introduces function f2 then atom f2[x] is the atom S(z; x), where z is some variable not used elsewhere. We define the set of all functions that may appear in the place of a bound variable v of an atom A when resolving any of its unfoldings with a non function free clause in (O) as follows: De nition 2. Let A be a function free atom, T a non empty subset of terms A and v a variable in vars A ∩ T . The function set Fv(A; T ) of all functions associated with A in variable v w.r.t. T is defined as follows:
{f | B(v) ∈ Dˆ(A; T ) and B(f (x)) ← atom f [x] ∈ (O)} ∪ Fv(A; T ) = {f | S(v; t) ∈ Dˆ(A; T ) and S(f (x); x) ← atom f [x] ∈ (O)} ∪ {f | S(t; v) ∈ Dˆ(A; T ) and S(x; f (x)) ← atom f [x] ∈ (O)}
It follows that (a) if A ≡ P (v; t) then f ∈ Fv(A; T ) iff (O) ⊢R P (f (t); s) ← atom f [t], (b) if A ≡ P (t; v) then f ∈ Fv(A; T ) iff (O) ⊢R P (s; f (t)) ← atom f [t], where in both cases s = t if t ∈ T otherwise either s = t, or s = g(f (t)) for some function g, and (c) if A ≡ A(v) then f ∈ Fv(A; T ) iff (O) ⊢R A(f (t)) ← atom f [t]. Again, T stands for the set of bound terms in A. 3.3
The shrinking step computes rewritings that can be inferred from the user query Q by eliminating one or more of its bound variables through their unification with a functional term. Given that the rewritings in rewr (Q; O) are function free, if a function is introduced in some rewriting during the standard resolution-based inference process, subsequently it must be eliminated. However, we know that each function appears in at most two clauses of (O), both of which have as body the atom atom f [x]. Now, the functional term f (x) can be introduced in a CQ only if some inference led to the substitution of a bound variable v by f (x). Hence, in order for f (x) to be eliminated, all atoms in which f (x) has been introduced must contain f in their function sets, for the appropriate argument. Moreover, if Q contains the terms say P (x; v) and P (v; y) and v is eliminated this way by unifying with f (x), variables x and y must be unified. If in place of x, y there are constants, these should coincide in order for the inference to be possible. This is the intuition behind the following shrinking inference rule: De nition 3. Let Q be a CQ and v a non distinguished bound variable of Q. Write Q in the form A ← B1; : : : ; Bk; C1; : : : ; Cn, where Bi are the atoms in body Q that contain v, and Ci the remaining atoms. Let also C = ∪k i=1 cons Bi and X = ∪ik=1(varsB Bi) \ v. The shrinking rule S on Q is defined as follows: A ← B1; : : : ; Bk; C1; : : : ; Cn f ∈ ∩ik=1 Fv(Bi; termsB Bi) ∧ |C| ≤ 1 cond (A ← atom f [t]; C1 ; : : : ; Cn ) where
= ∪x∈X {x=t}, and t = a if C = {a} otherwise t is a variable ∈= vars Q. 3.4
Let S∗(Q) be the closure of cond Q under application of the inference rule S, for any CQ Q. By construction, S∗(Q) contains a ‘representative’ for all query structures that can result from Q by eliminating one or more variables in varsB Q by using functional terms. This representative can be considered as a ‘top’ query, in the sense that in can produce several more CQs with no further structural changes due to bindings of bound variables with functional terms. Hence, the remaining rewritings can be obtained by computing, for each Q′ ∈ S∗(Q), all CQs that can be inferred from Q′ by replacing one or more of its atoms by one of their unfoldings. In this way we can eventually compute all rewritings of Q. This can be achieved by applying the following unfolding inference rule: De nition 4. An unfolding of CQ Q : A ← B1; : : : ; Bn, is the conclusion of any application of the following unfolding rule W:
A ← B1; : : : ; Bn Ci ∈ Dˆ(Bi; termsB Bi) for i = 1 : : : n
cond (A ← C1 1; : : : ; Cn n) x ∈ varsUB Ci. where i is a renaming of varsUB Ci such that x i ∈= ∪n j=1;j̸=i vars (Cj j ) for all
Let W∗(Q) be the closure of a cond Q under application of the inference rule W, for any Q. The strategy by which Rapidf computes the core rewriting set of a user query Q is justified by the following theorem: Theorem 1. Let Q be a CQ over a DL-LiteR ontology O.
If Q′ ∈ ∪Q′′∈S∗(Q) W∗(Q′′) then Q′ ∈ˆ rewr (Q; O) (soundness), and if Q′ ∈ rewrC (Q; O) then Q′ ∈ˆ ∪Q′′∈S∗(Q) W∗(Q′′) (completeness). 3.5
If we apply exhaustively the W rule in order to compute W∗(Q), we may end up with many subsumed rewritings. Because the subsumption check operation needed to remove them is very costly, Rapidf applies W in a cleverer way, so as to get as few as possible subsumed rewritings. In fact, it restates the unfolding problem as follows: Given a CQ Q of the form A ← B1; : : : ; Bn, find the non subsumed CQs that are conclusions of all possible applications of W on Q. For convenience, define Bi = Dˆ(Bi; termsB Bi), so that we get the sequence of the possibly non disjoint unfolding sets B1; : : : ; Bn. For simplicity, we drop the substitutions i in Def. 4 by assuming that each time a rule of J (T ) that introduces a new variable is applied, this variable does not appear elsewhere.
For any B ∈ ∪in=1 Bi, define the set ind B = {j | B ∈ Bj } of the indices of all unfolding sets that contain B. We call the set C =: {C1; : : : ; Ck} with k ≤ n a selection for Q iff (a) ∪ik=1 ind Ci = Nn, where Nn = {1; : : : ; n}, and (b) ind Ci \ ind Cj ̸= ∅ for all i; j ∈ Nk, i.e. if C contains at least one atom from each unfolding set and no two sets ind Ci overlap fully. Clearly, a selection corresponds to an unfolding of Q, in particular to A ← C. However, of interest are the minimal selections, which can produce non subsumed rewritings. We call a selection C for Q minimal, iff there is no selection C′ for Q such that C′ ⊂ C, i.e. if condition (b) above is replaced by the stronger condition ind Ci \ (∪jk=1;j̸=i ind Cj ) ̸= ∅ for all i ∈ Nk, i.e. if all atoms Ci need to be present in set C in order for ∪k
i=1 ind Ci = Nn to hold. If this were not the case, we could form the selection C′ = {C1; : : : ; Ci−1; Ci+1; Ck} ⊂ C, hence C would not be minimal.
In this computation of minimal selections only equality between the elements of the sets Bi is taken into account, and not subsumption relations. However, an unfolding set may contain an atom with an unbound variable (e.g. P (x; ∗), where ∗ is unbound) which unifies with an atom of another unfolding set that contains only bound variables (e.g. P (x; y)). The unfoldings of a CQ Q resulting after such unifications are made may subsume or be subsumed by several of the unfoldings given directly by other minimal selections for Q. In order to take into account atom subsumption relations, we compute all possible bindings for the unbound variables that appear in the sets Bi in advance and enrich the respective sets Bi with the respective atoms, before computing the minimal selections. In particular, if for some i; j ∈ Nn we have C ∈ Bi and C′ ∈ Bj and there is a substitution on varsUB C′ such that C′ = C, we add C to Bj. The presence of any such two atoms C′ and C in any pair Bi; Bj, regardless of whether they were present from the beginning or introduced at the enrichment phase, establishes a parent-child relationship between C′ and C. Let parents C and children C denote the set of parent and child atoms of atom C across all the sets Bi. Obviously, a child can have several parents in different unfolding sets, possibly distinct between each other, and the same holds for the children of a parent.
In order to avoid the production of subsumed rewritings due to such atom subsumptions, for each candidate unfolding Q : A ← C obtained from a minimal selection C, Rapidf performs two checks: (1) For each parent C of an atom in C, it constructs a candidate rewriting with body C′ = {C} ∪ (C \ children C), i.e it replaces all children of C by their parent. If C′ is a minimal selection, then Q is discarded because it is subsumed by A ← C′. E.g. Q(x) ← S(x; y); T (x; y) is subsumed by Q(x) ← S(x; ∗); T (x; z) where S(x; y) is a child of S(x; ∗). (2) For each atom C that is a child of an atom in C it constructs the candidate body C′ = {C} ∪ {D | D ∈ C and ind D * ind C}, i.e. it replaces the parent by its child C and keeps all the remaining atoms of C that are not ‘covered’ (in terms of their indices) by C. If cond (A ← C′) ◃ Q then Q is discarded because it is subsumed. E.g. Q(x; y) ← R(x; y); S(y; w); T (y; z); S(v; z) is subsumed by Q(x; y) ← R(x; y); S(y; z), where S(y; z) is child of both S(y; w) and S(v; z).
The only case an unfolding Q′ of Q obtained in this way may subsume another unfolding of Q is when the condensation of Q′ does not contain one or more of the variables in varsB Q; this implies that a structural change has happened to cond Q′. To cover this case, we always compute the condensation of each unfolding given by the above procedure. If the condensation does not contain a bound variable of Q it is marked as impure, otherwise as pure. Given that the unfolding step is executed for each rewriting produced by the shrinking step, the final step is the check for subsumed rewritings within the results of the entire unfolding process. The check is done after first grouping the results into sets that are known not to contain subsumed rewritings. As explained, these are the sets of pure unfoldings obtained during the unfolding step for each rewriting given by the shrinking step. Each impure unfolding is considered to be a separate set.
The overall structure of Rapidf for a user query Q is shown in Algorithm 1. Procedure Shrink computes S∗(Q), by iteratively applying Def 3. For each rewriting computed by Shrink, procedure Unfold computes its minimal selections and discards any subsumed unfoldings as described above. Finally, the unfoldings, grouped into sets of pure unfoldings and singleton sets of impure unfoldings, are processed by procedure CheckSubsumption, which checks for subsumptions across sets only and removes any subsumed rewritings.
procedure Rapidf (CQ Q, ontology O) Qf = ∅ for all Qs ∈ Shrink(Q; O) do
Qt ← ∅ for all Q′ ∈ Unfold(Qs; O) do if varsB Q ⊆ vars (cond Q′) then
Qt ← Qt ∪ {Q′} else
Qf ← Qf ∪ {{cond Q′}} end if end for
Qf ← Qf ∪ {Qt} end for return CheckSubsumption(Qf ) end procedure
The side premises Ci ∈ Dˆ(Bi; termsB Bi) of the unfolding rule W may be seen
as the clauses Ci ← Di for some Di ∈ Dˆ(Bi; termsB Bi). Hence, similarly to
[
First, we can remove from the body of the several Q′ ∈ S∗(Q) the atoms that will certainly produce only subsumed rewritings (in the case we were to apply exhaustively the W rule, as before, in order to compute all rewritings); this happens if there are two atoms A; B ∈ body Q′ and a such that A = C for some C ∈ D(termsB B), i.e. if A is subsumed by C. In this case we just remove B from body Q′. Let rr (S∗(Q)) be the set of clauses obtained in this way from S∗(Q) and also after removing from it any subsumed clauses.
Next, we must construct the set of clauses U . This is straightforward, but we must take into account the different bindings that bound and unbound variables can have during the unfolding. So, for all atoms A that appear in the clauses of rr (S∗(Q)) we compute the set D(A; varsB A) and then we construct from A a new atom A′ by removing from the arguments of A all unbound variables and replacing the predicate p of A by a new predicate pt1 or pt1t2 , if A is a concept or role atom, respectively, and ti = 0 if the i-th argument of A is unbound and A′ ←
D for all D ∈ D(A; varsB A). ti = 1 otherwise. Finally we normalize the clauses in rr (S∗(Q)) by replacing all appearances of A by A′, and add to U the clause A′ ← A as well as the clause
PQ is the union of U and the normalized version of all clauses in rr (S∗(Q)). 4
We evaluated Rapidf by comparing it with Rapid and Requiem, the
implementation of RQR. We used the same datasets as in [
The results show clearly the efficiency of Rapidf . It is always faster than Rapid, and much faster than Requiem; in several cases the improvement is significant. The most striking case is ontology AX and query 5, in which Rapidf completes the computation of the 32,921 core rewritings in less than 4 seconds, while Rapid needs 50 seconds and Requiem about 2 hours. The more detailed study of this particular case showed that Rapidf computes directly the final core rewriting set and performs no subsumption checks at all. On the other hand, Rapid spends about 45 seconds checking for subsumptions and Requiem about 1.5 hours.
Table 3 also shows, as expected, that Rapidd is always much faster than any
of the other algorithms, since it does not include the unfolding step, which is
the main source of complexity, even for the optimized Rapidf algorithm. For
the same ontologies and query pairs tested in [
We presented Rapidf , an efficient algorithm for the computation of the core
rewriting set of queries posed over DL-LiteR ontologies. Rapidf optimizes the
inference process by replacing the application of the first order resolution rule
by specialized shrinking and unfolding rules, which save the algorithm from
many unnecessary rewritings, subsumption checks and blind inference paths.
We presented also Rapidd a modification of Rapidf , which does not unfold the
rewritings, but encodes the unfoldings into a datalog program similarly to [