In recent years, there has been a growing interest in the problem of conjunctive query answering over description logic (DL) ontologies and large scale data sets. This problem is central to many applications, which often involve managing data sets consisting of hundreds of millions, or even billions of data assertions.
Meeting the scalability requirements of such applications is, however, a very challenging problem. Answering conjunctive queries over ontologies in expressive DLs is of high computational complexity; in fact, decidability is still an open problem for SROIQ [14] -the DL that underpins the standard ontology language OWL 2 [6]. Although small restriction on the ontology or query language can ensure decidability [26], worst case complexity is still very high (at least 2NExpTime) [15]. Several OWL/SROIQ reasoners, including Her-miT [20], FaCT++ [28] and Racer [12], support query answering for restricted classes of conjunctive queries, but in spite of intensive efforts at optimisation, they can still only deal with small to medium size data sets [17,13].
Scalability of query answering can be ensured by restricting the expressive power of the ontology language to the level that makes reasoning tractable. This has led to the development of three profiles of OWL 2, namely OWL 2 RL, OWL 2 EL, and OWL 2 QL [21]; these profiles are based on (families of) "lightweight" description logics, notably the DLP [10], DL-Lite [4], and the EL families of DLs [2], respectively. Query answering in all these lightweight DLs can be implemented in polynomial time w.r.t. the size of data (and even in LogSpace in the case of DL-Lite). Such appealing theoretical properties have spurred the development of specialised reasoning techniques [24,22,18,4,16].
Although allowing for efficient query answering, these lightweight DLs impose severe restrictions on the expressive power of the ontology language. In order to provide scalable query answering w.r.t. ontologies that cannot be captured by such lightweight DLs, Semantic Web researchers have developed reasoners that can process arbitrary OWL/SROIQ ontologies, but that guarantee completeness only for ontologies that fall within the fragment defined by the OWL 2 RL profile. Given the close connection between OWL 2 RL and datalog, these reasoners typically implement (deductive) database algorithms based on data materialisation. Examples of such systems include Jena [19] and OWLim [16].
All such materialisation-based reasoners are sound ; that is, the answers they compute can be seen as a lower bound on the complete set of query answers.
For ontologies outside the OWL 2 RL profile, however, these reasoners are incomplete, and hence they are not guaranteed to compute all query answers. A possible approach to this problem is to investigate the behaviour of the reasoner on a given query Q and ontology T in an effort to show that it behaves as a complete reasoner w.r.t. Q, T and an arbitrary data set [7]. Providing such guarantees is, however, not always possible.
An alternative approach, which we investigate in this paper, is to devise a scalable procedure for computing complete but possibly unsound query answers. Such answers provide an upper bound to the set of all answers, which can complement the lower bounds efficiently computed by incomplete reasoners. The combined use of such lower and upper bounds has many interesting implications. First, the difference between the upper and lower bounds can be used as an optimisation for reducing the number of candidate answers; furthermore, it also provides a measure of the degree of incompleteness of a reasoner for a given input; finally, if both bounds match, we can efficiently compute all query answers without relying on potentially very expensive entailment tests.
In order to be useful, upper bounds should clearly be as tight as possible, and should also be efficiently computable. Obtaining such an upper bound is, however, not straightforward. The technique we use is to approximate T to give an ontology T that is strictly "stronger" that T (i.e., T |= T ), and that is within a fragment for which query answers can be efficiently computed.
Knowledge approximation has been extensively studied in the literature, although mostly in the direction of weakening the ontology/theory [8,23]. There has also been some work on strengthening approximations. For propositional logic, Horn theories can be used to both strengthen and weaken the original theory [27]; these Horn approximations can then be used to optimise reasoning by exploting the more efficient inference in the Horn theories. Finally, approximation is also related to the computation of least common subsumers [1].
Our technique exploits recent work on chase termination for existential rules, which introduces a so called Models-Summarising Acyclicity (MSA) check [5]. MSA is an approximation of existential rules (datalog ± ) into datalog. As most SROIQ TBoxes can be translated into existential rules extended with disjunction (datalog ±,∨ ) using model-preserving transformations, we can adapt MSA to produce a datalog approximation of a SROIQ TBox. Moreover, the resulting datalog rules can be translated back into an OWL 2 RL TBox for which complete query answers can be computed using materialisation based reasoners.
We have implemented our approach, and conducted preliminary experiments using LUBM [11]. Our preliminary results suggest that our bound could be tight for many queries, and it can be computed efficiently (or at least with similar efficiency to computing the lower bound).
We assume basic familiarity with the DLs underpinning the ontology language OWL 2 and its profiles. We next introduce datalog ±,∨ and datalog languages, and define the syntax and semantics of conjunctive queries. In our definitions, we adopt standard first-order logic notions of variable, constant, term, substitution, atom, formula, and sentence. We assume all formulas to be function-free. We denote with ⊥ the special atom evaluated as false in all interpretations, and we use ≈ to denote the special equality predicate in first-order logic. Finally, we also adopt the standard notions of satisfiability, unsatisfiability, and entailment. Datalog Languages. A datalog ±,∨ rule r is a formula of the form (1), where each B j is an atom different from ⊥ whose free variables are contained in x, and
A rule is safe if each variable in x also occurs in some B j , and we consider only safe rules. For brevity, the quantifier ∀x is left implicit. The body of r is the set body(r) = {B 1 , . . . , B n }, and the head of r is the formula head
, and it is datalog if it is datalog ± and the head is a single atom without existential quantifiers.
A fact is a ground atom, and an instance I is a finite set of facts. We denote with ind(I) the set of all individuals occurring in I.
For Σ a set of datalog rules and I an instance, the saturation of Σ w.r.t. I is the instance I consisting of all facts entailed by Σ ∪ I.
Most DL ontologies can be transformed into a set of datalog ±,∨ rules and an instance by means of standard transformations. The rules and facts obtained via such transformations involve only unary and binary predicates; thus, we define an ABox A as an instance containing only unary and binary atoms.
Queries. A conjunctive query (CQ), or simply a query, is a formula Q(x) of the form ∃y.ϕ(x, y), where ϕ(x, y) is a conjunction of atoms. A tuple of individuals a is a certain answer to a query Q(x) w.r.t. a set of first-order sentences F and an instance I if F ∪ I |= Q(a). The set of answers of Q(x) w.r.t. F and I is denoted as cert(Q, F, I), where the free variables of Q(x) are omitted for brevity.
Given a TBox T , an ABox A and a query Q, our goal is to compute a (hopefully tight) upper bound to the set cert(Q, T , A) of answers. We poceed as follows:
1. Transform T into a set Σ T of datalog
for every query Q and ABox A.
Our transformation depends only on T , and satisfies the following property:
Given the OWL 2 RL TBox T we can then use T and T with a materialisation based reasoner rl that is sound for OWL 2 and complete for OWL 2 RL (such as OWLim) to respectively compute a lower and an upper bound to query answers for the given Q and A. More precisely, we have:
for every Q and A
We next describe in detail the transformations in Steps 1-3. As a running example, we use the TBox T ex in Figure 1.
From DL TBoxes to Datalog ±,∨ Rules. The first step is to transform the DL TBox T into a set Σ T of datalog ±,∨ rules such that Σ T is a conservative extension of T . For a wide range of DLs, this can be achieved by first using the well-known correspondence between DL axioms and first-order logic formulas and then applying standard structural transformation rules, which may involve introducing new predicates. The transformation of our example T ex into datalog ±,∨ rules Σ Tex is also shown in Figure 1; here, T ex and Σ Tex are equivalent.
From Datalog ±,∨ to Datalog. Next, we approximate the datalog ±,∨ rules Σ T by a datalog program approx(Σ T ) that entails Σ T . Intuitively, this transformation can be described in two steps:
-Rewrite each datalog ±,∨ rule r into a set of datalog ± rules by transforming disjunctions in the head of r into conjunctions and splitting the conjunctions into different datalog ± rules. Such a way to eliminate disjunction in the head has been used in OWL reasoning with logic program [25]. -Transform the resulting datalog ± rules into datalog using fresh individuals to skolemise existentially quantified variables.
Figure 2 illustrates this process for our example. The figure shows only the rules in Σ Tex that need changing; note that c 1 and c 2 are fresh individuals used to skolemise existentially quantified variables. 1Definition 1. For each datalog ±,∨ rule r of the form (1) and each variable y ij ∈ y i , let c r ij be a fresh individual unique for r and y ij . Then, approx(r) is the following set of rules, where for each 1 ≤ i ≤ m, θ r i is a substitution mapping each variable y ij ∈ y i to c r ij :
For Σ a set of datalog ±,∨ rules, approx(Σ) is the smallest set that contains approx(r) for each rule r ∈ Σ.
We next show that approx(Σ T ) entails Σ T . The following proposition provides sufficient and necessary conditions for a datalog ±,∨ rule to be entailed by an arbitrary set of first-order sentences (the proof is rather straightforward and can be found in [7]). Proposition 1. Let F be a set of first-order sentences and r be a datalog ±,∨ rule of the form (1). Then, for each substitution σ mapping the free variables of r to distinct individuals not occurring in F or r, we have F |= r if and only if
Proposition 1 can be used to show that each datalog ±,∨ rule r in Σ T is entailed by approx(r), and hence approx(Σ T ) strengthens Σ T . Proposition 2. For Σ a set of datalog ±,∨ rules, we have approx(Σ) |= Σ.
Proof. It suffices to show that, for each rule r ∈ Σ of the form (1) and each r i ∈ approx(r), we have r i |= r. Let σ be a substitution mapping the free variables in r to fresh individuals; by Proposition 1, we have
Since r i and r have the same body atoms, the definition of r i in (2) implies
Since substitution θ r i maps variables to constants, the following conditions clearly hold by the semantics of first-order logic:
But then, conditions (3), ( 4) and ( 5) immediately imply r i |= r, as required.
The fact that approx(Σ) entails Σ implies that query answers w.r.t. approx(Σ) are an upper bound to those w.r.t. Σ.
Proposition 3. For each set of datalog ±,∨ rules Σ, each ABox A and each query Q, we have cert(Q, Σ, A) ⊆ cert(Q, approx(Σ), A).
From Datalog to OWL 2 RL. The last step is to transform approx(Σ T ) into an OWL 2 RL TBox T . Although arbitrary datalog rules cannot be transformed into OWL 2 RL, the rules in approx(Σ T ) have been obtained from a DL TBox and are therefore tree-shaped, which makes this transformation possible. There is, however, a technical consideration related to the fresh skolem constants in approx(Σ T ). In particular, the following rule in our running example (see Figure 2) does not directly correspond to an OWL 2 RL axiom:
This issue can be easily addressed by introducing fresh atomic roles. More precisely, rule (6) can be transformed into the following three OWL 2 RL axioms, where R is a fresh atomic role:
RA ∃R .{c 1 } ∀R .Group R works
Transformation of Disjunctive Rules. The proof of Proposition 2 suggests that we can easily weaken approx(Σ T ) given in Definition 1 such that Σ T is still entailed. In particular, when transforming a disjunctive rule in Σ T into datalog by replacing disjunctions with conjunctions, it suffices to keep only one of the conjuncts. For example, given the transformation
we can replace in approx(Σ T ) the rule Student(x) → Grad(x) ∧ Undergrad(x) with either Student(x) → Grad(x), or Student(x) → Undergrad(x). Any of these choices will lead to a (different) upper bound. In practice, one can choose to process any number of such different options, or simply devise suitable heuristics to choose the most promising one.
Unsatisfiability Issues. For given TBox T and ABox A, it might be the case that approx(Σ T ) ∪ A is unsatisfiable, whereas Σ T ∪ A is satisfiable. Then, the upper bound we obtain is the trivial one for each query. For example, if we extend T ex in Figure 1 with the axiom Grad Undergrad ⊥, we obtain a rule with ⊥ in the head in Σ T , namely Grad(x) ∧ Undergrad(x) → ⊥. For A ex = {RA(a)} we then have that T ex ∪ A ex is satisfiable, but approx(Σ Tex ) ∪ A ex is unsatisfiable; thus, for a given Q, any tuple of individuals of the appropriate arity must be included in the upper bound.
A way to address this issue is to remove from approx(Σ T ) all rules with ⊥ in the head. Although it is then no longer the case that approx(Σ T ) |= Σ T , we can still guarantee completeness provided that Σ T ∪ A is satisfiable. Proposition 4. Let Σ be a set of datalog ±,∨ rules and let Σ the result of removing from approx(Σ) all rules containing ⊥ in the head. Then, the following condition holds for each ABox A and each query
In practice, checking the satisfiability of T ∪A, which is equisatisfiable with Σ T ∪ A, is easier than (and a prerrequisite for) query answering. Even if satisfiability of T ∪ A cannot be checked in practice using a complete reasoner for a very large A, we can still compute an upper bound "modulo satisfiability".
Why Translating Back into OWL 2 RL? Our last step was to transform approx(Σ T ) into OWL 2 RL TBox T . Note, however, that one could obtain the upper bound directly from approx(Σ T ) by first computing the saturation A of approx(Σ T ) w.r.t. A and then computing cert(Q, ∅, A ).
The saturation A can be computed in polynomial time [5]; indeed, the rules in approx(Σ T ) are tree-shaped, which can be exploited to obtain a polynomial time saturation procedure. This could lead to better performance in the computation of our upper bound -an interesting topic for future work.
Our current approach, however, does have some advantages. In particular, one can use the same off-the-shelf RL reasoner (such as OWLim) to compute both the lower and upper bound, which is convenient in practice. Furthermore, as suggested by our experiments, reasoners such as OWLim are quite efficient for large data sets.
We have implemented our approach in Java and used the latest version of OWLim-Lite as an OWL 2 RL reasoner. All experiments have been performed on a desktop computer with 4Gb of RAM, of which 3000Mb were assigned as maximum heap size in Java.
In our experiments, we have used LUBM extended with additional synthetically generated queries. The LUBM ontology contains 93 TBox axioms, out of which 8 contain existential quantification, and 39 are domain and range axioms. The LUBM ontology, however, does not contain disjunction or negation; thus, 1, the lower and upper bounds computed using OWLim coincide, which allows us to conclude that OWLim is complete for all these queries and the LUBM(1,0) data set. Hence, in these cases, one wouldn't need to use a complete DL reasoner at all.
Additional Synthetic Queries. We have used a synthetic query generation tool [9] to compute 78 additional queries for LUBM. For all these queries, except those in Table 2, lower and upper bounds also coincide. Furthermore, for all queries in Table 2 the upper bound is tight. Observe, however, that the lower bound is missing those answers which require taking into account LUBM's axioms with existential quantifiers, for which OWLim is not complete. For example, consider the following query Q 51 (x) = ∃y.(memberOf(x, y) ∧ Group(y)) LUBM's ontology contains all the axioms in T ex , except for the last two axioms in Figure 1; furthermore, LUBM(1,0) contains many instances of RA. Since LUBM's ontology implies that each RA works for (and hence is a member of) some group, all these instances are answers to Q 51 , which are not computed by OWLim.
Additional Query. For all previous test queries, we have obtained a tight upper bound. To show that this is not always the case, we have manually created the additional query given next. Q(x 1 , x 2 ) = ∃y.works(x 1 , y) ∧ works(x 2 , y) ∧ Group(y) Since this query is not tree-like, it cannot be answered using HermiT. To obtain the complete answers, we have used REQUIEM2 to compute a (complete) UCQ rewriting U of Q w.r.t. LUBM's ontology; then, we used OWLim to compute the answers to U w.r.t. the LUBM(1,0) data. For this query, the lower and upper bounds contained zero and 299, 209 answers, respectively; in contrast, we obtained 547 answers using REQUIEM and hence the upper bound is not tight.
As shown in Figure 2, our transformation implies that all RAs work for the same group (represented by the skolem constant c 1 ); since there are many instances of RA in LUBM(1,0), all pairs of RA instances will be included in the upper bound. Clearly, however, many of these RAs work for different groups.
Note, however, that even for this query we managed to reduce the number of candidate answers from 17, 174 2 ∼ 3 × 10 8 to 299, 209.
To test scalability of upper bound computation, we have performed additional experiments using LUBM data sets of increasing size (from 1 to 10 universities). For each data set and each of the 78 synthetic queries, we have computed lower and upper bounds (using OWLim) and the complete answers (using HermiT). The results are summarised in Figure 4.2, where the time refers to the total query answering time for all test queries.
We can observe similar query answering times and scalability behaviour for lower and upper bound computation. Furthermore, we can observe that Her-miT's performance is similar to OWLim's for relatively small data sets. HermiT, however, does not scale well for the largest LUBM data sets. In particular, it takes 178s to complete the tests for 9 universities and runs out of memory for 10 universities; in contrast, OWLim computation times increase more regularly.
In this paper, we have proposed a novel technique for efficiently computing an upper bound to CQ answers for ontologies given in a expressive DL. Our preliminary experiments on LUBM show that this upper bound might be tight in many cases. Furthermore, we identified cases were lower and upper bounds coincide and hence it is not necessary to use a fully-fledged DL reasoner such as HermiT to compute query answers (HermiT is able to answer rollable queries).
Our work so far, however, is only very preliminary, and there are plenty of possibilities for future work. We are planning to perform experiments with ontologies involving disjunction and negation, and address the issues discussed in Section 3.3. Furthermore, we will implement a dedicated datalog engine that can compute the saturation in polynomial time for tree-shaped datalog rules; this might allow us to improve performance as well as to simultaneously compute lower and upper bounds. We will also develop techniques for identifying during upper bound computation the fragments of the ABox and TBox that are sufficient to determine, using a complete reasoner, which of the answers in the upper bound are actual answers; we expect that these techniques will provide additional room for optimisation. As a result, we can integrate all these techniques in HermiT to optimise query answering.
Acknowledgements. This work was supported by the Royal Society, the EU FP7 project SEALS and the EPSRC projects ConDOR, ExODA, and LogMap.