What to Ask to an Incomplete Semantic Web Reasoner?

1 Introduction

Ontology schemas (or TBoxes) are often used for describing the meaning of data stored in various sources. In this setting, query languages are based on conjunctive queries (CQs), with the ontology providing the vocabulary used in queries [Glimm et al., 2007; Lutz et al., 2009; Calvanese et al., 2007].

Largely motivated by Semantic Web applications, there has been a growing interest in the development of ontology-based query answering systems that are highly scalable in practice, but that are incomplete, i.e., they are not guaranteed to compute all query answers for some combinations of queries, ontologies, and datasets accepted as valid inputs. Examples of widely-used such systems are Oracle's Semantic Data Store, Jena, DLEJena, OWLim, Minerva and Sesame.

A challenge when using incomplete systems is to evaluate the scalability-completeness trade-off exhibited by different systems for a given application. As recently pointed out [Stoilos et al., 2010b], the use of existing performance evaluation benchmarks, such as LUBM [Guo et al., 2005], has serious limitations for this purpose. In particular, results using these benchmarks tell us little about the system's behaviour for the application at hand: they are limited to a specific ontology schema (the LUBM TBox about an academic domain), queries (LUBM contains a fixed pre-computed set of 14 sample queries), and datasets (a fixed number of relational structures hard-coded into the benchmark's scripts). Furthermore, correct answers can only be measured by comparison with the output of a complete system, and cannot be verified for large datasets that no complete system can handle.

The framework in [Stoilos et al., 2010b; 2010a] partly addresses these limitations. The intuition behind these works is that given a TBox T and query q, it may be possible to compute a finite collection of datasets, called a testing base, such that if a system is complete for T , q and each dataset in the collection, then it will also be complete for any dataset. In this case, one could say that an incomplete system is (q, T )- complete-that is, it behaves exactly like a complete reasoner w.r.t. q and T , and regardless of the data (which is typically unknown and/or frequently changing). Furthermore, answers for each dataset in a testing base are known at generation time (thus, easy to verify), and the framework also provides a quantitative measure of completeness that makes comparison between different systems possible. Although there are ontologies and queries for which such testing base would necessarily be infinite, Stoilos et al. also identified sufficient conditions on T and q under which a (finite) testing base is guaranteed to exist and provided algorithms for computing it.

This framework, however, relies on the assumption that both the TBox and queries of interest are known. Although in many applications the TBox is under the control of the application developers, queries depend on users' needs and application developers may only have a rough idea of which ones might be of particular relevance. Consequently, the assumption that test queries should be fixed in advance for evaluation purposes is likely to be too strict a requirement.

In this paper, we address this limitation and develop a novel framework in which completeness evaluation depends only on the application's TBox T , and not on a set of pre-defined queries. More precisely, given T , we study the problem of generating a finite collection of conjunctive queries (a query testing base), such that if a system is (q, T )-complete for each query q in the collection, then it will also be (q′ , T )-complete for any arbitrary query q′ . As well as providing a new quantitative measure of completeness depending only on T , this would allow us to identify circumstances under which an incomplete reasoner is indistinguishable from a complete one for a particular TBox T , regardless of the user's query and input data. As a result, application developers would be able to assess with a much higher degree of confidence whether a given systemmeets their needs.

In practice, our framework relies on the techniques developed in [Stoilos et al., 2010b] and [Stoilos et al., 2010a] in order to check whether a system is (q, T )-complete for each q in a query testing base (and hence we are subject to their same practical limitations). Conceptually, however, we are addressing a very different problem since we are interested in automated query generation, rather than in data generation.

It is worth emphasising that automated query generation is an active research topic in databases [Poess and Stephens, 2004; Khalek and Khurshid, 2010]. The focus in the database literature, however, is on performance evaluation rather than on completeness of the evaluated query engines.

The main contributions of this paper are as follows:

• We extend the framework in [Stoilos et al., 2010b] with the notion of a query testing base.
• We explore the limitations of the new framework and formulate precise conditions under which a query testing base would necessarily be infinite.
• We identify sufficient conditions on T for which a (finite) query testing base can be efficiently obtained. Interestingly, such sufficient conditions are strongly related to the notion of weak acyclicity, which is widely used in the context of data exchange [Fagin et al., 2005].
• We present query generation algorithms for the logics underpinning the QL, EL and RL profiles of the new standard ontology language OWL 2 [Motik et al., 2009].
• We provide preliminary empirical evidence suggesting that our framework is feasible in practice.

This paper is accompanied with an online technical report containing complete proofs and additional technical details. 1

2 Preliminaries

Description Logics We assume basic familiarity with DL syntax, semantics and standard reasoning problems.

When in Section 3 we speak of an arbitrary description logic L, we refer to a fragment of the DLs underpinning OWL and OWL 2. We use standard notions of an L-TBox T (the schema), an L-ABox A (the data), and an L-ontology O = T ∪ A, but assume that ABoxes contain only atomic assertions of the form A(a) or R(a, b), with A and R atomic. Also, we sometimes use the standard notion of homomorphism (isomorphism) between ABoxes. Finally, to avoid conflating schema and data, we only consider DLs without nominals (i.e., that do not allow individuals in the TBox).

We next recapitulate the syntax of the concrete DLs mentioned in Section 4, namely DL-Lite 2 [Calvanese et al., 2007] and EL [Baader et al., 2005], which provide the logical underpinning for the QL and EL profiles of OWL 2.

A role is an atomic role R or its inverse R-. The function ar(R, a, b) takes a role R and individuals a, b, and returns R(a, b) if R is atomic, or P(b, a) if R = P -, with P atomic. A DL-Lite-concept B is either atomic, or of the form ∃R.⊤ with R a role. A DL-Lite-TBox is a finite set of GCIs of the form B1 ⊑ B2 (positive GCI), or B1 ⊑ ¬B2 (negative GCI), with B1 and B2 DL-Lite concepts.

1 http://ijcai2011.tripod.com/querycompleteness.pdf

2 The logic used in this paper is the simplest one among those in the DL-Lite family, and it is commonly referred to as DL-Litecore.

The set of EL-concepts is given by the following grammar, where A, R are atomic and C(i) are EL-concepts:

An EL-TBox T is a finite set of GCIs of the form C1 ⊑ C2 with C1 and C2 EL-concepts. We use the notation C1 ≡ C2 as an abbreviation for C1 ⊑ C2 and C2 ⊑ C1. We assume from now on that EL-TBoxes are normalised, i.e., that each GCI in T is in one of the following forms, with A(i) atomic or ⊤, and R atomic: A1 ⊑ A2, A1 ⊓ A2 ⊑ A, A1 ⊑ ∃R.A2, or ∃R.A2 ⊑ A1.

The DLs considered in this paper can be seen as fragments of First-Order Logic (FOL), and their semantics is standard [Baader et al., 2002]. The definitions of reasoning problems such as consistency and entailment are also standard.

Conjunctive Queries We use standard notions of (functionfree) term and variable. A concept atom is of the form A(t) with A an atomic concept and t a term. A role atom is of the form R(t, t′ ) for R an atomic role, and t, t′ terms. A conjunctive query (CQ) q is an expression of the form

where each αi is a concept atom or a role atom and each xj is a distinguished variable occurring in some αi. A certain answer to q w.r.t. O = T ∪ A is a tuple c = 〈c1, . . . , cn〉 of individuals such that O entails the FOL formula obtained by building the conjunction of all atoms αi in q, replacing each distinguished variable xj with cj and existentially quantifying over the remaining variables. We denote with cert(q,O) the set of all certain answers to q w.r.t. O. Finally, we sometimes use the well-known notions of homomorphism from a query q to q′ and between a CQ and an ABox.

The Chase CQ answering in L ∈ {DL-Lite, EL} can be characterised according to the notion of chase, adapted from database dependency theory. Given a consistent L-ontology O = T ∪A, chaseL(O) is a (possibly infinite) forest-shaped ABox constructed step-by-step from A and which represents all models of O for the purpose of CQ answering. More precisely, cert(q, O) = cert(q, chaseL(O)), where we abuse notation and use cert(q, chaseL(O)) to represent those answers to q w.r.t. chaseL(O) containing only individuals from A (which we call named chase individuals from now on).

The chase construction rules for DL-Lite and EL are given in [Calvanese et al., 2007] and [Rosati, 2007], respectively. They are also given in a compact way in our technical report.

3 Framework

We next present our query generation framework. We start by recalling the notion of a CQ answering algorithm given in [Stoilos et al., 2010b], which will allow us, on the one hand, to abstract from the specifics of implemented systems and, on the other hand, to establish general results that hold for any system satisfying certain basic properties.

Definition 1. A CQ answering algorithm ans for a DL L is a procedure that, for each L-ontology O and CQ q computes in a finite number of steps a set of tuples ans(q,O) of the same arity as the certain answers to q.

It is sound if, for each O and q, ans(q,O) ⊆ cert(q,O), and it is complete if cert(q,O) ⊆ ans(q,O).

It is monotonic if ans(q,O) ⊆ ans(q,O′ ) for each q, O and O′ such that O ⊆ O′ .

It is invariant under renamings if, for each q, O = T ∪A, and O′ = T ∪A′ with A and A′ isomorphic, ans(q,O) and ans(q,O′ ) are identical modulo the same isomorphism.

Finally, ans is well-behaved if it is sound, monotonic and invariant under renamings.

Intuitively, a well-behaved algorithm implements the semantics of CQ answering faithfully: query answers can only grow if we add axioms to the ontology, and they cannot depend on trivial renamings of ABox individuals. This allows us to rule out "unreasonable" algorithms at this level of generality. All incomplete systems known to us are well-behaved.

We next recall the notion of completeness for a fixed query q and TBox T studied in [Stoilos et al., 2010b; 2010a].

Definition 2. Let L be a description logic, q a CQ, T an LTBox and ans a CQ answering algorithm for L. We say that ans is (q, T )-complete if for each ABox A s.t. O = T ∪ A is consistent, we have that cert(q, O) ⊆ ans(q, O).

We can then introduce our notion of a query testing base: a set of CQs for a TBox T that we can use to ensure that an incomplete reasoner behaves exactly like a complete one for T , regardless of the input query and data.

Definition 3. Let L be a description logic, and let T be an L-TBox. A Query Testing Base (QTB) Q for T and a class CL of CQ answering algorithms for L is a finite set of CQs such that the following property holds for each algorithm ans in C L: If ans is (q, T )-complete for each q ∈ Q, then it is also (q′ , T )-complete for each CQ q′ .

To make our results as general as possible, we have parameterised QTBs w.r.t. a given class of algorithms-that is, a family of algorithms that share certain properties.

Unfortunately, as shown by the following theorem, QTBs fail to exist even for the empty ontology because such a QTB would need to contain infinitely many queries.

Theorem 4. Let L be a DL. No QTB exists for T = ∅ and the class of well-behaved CQ answering algorithms for L.

Proof. Let Q be an arbitrary, but finite, set of CQs and let m be the maximum number of variables in a query from Q. Consider also the following query:

We provide a well-behaved algorithm ans for L that is (p, ∅)- complete for each p ∈ Q, but it is not (q, ∅)-complete, which proves our theorem. Let ans proceed as follows when given a CQ qin and an L-ontology Oin = Tin ∪ Ain:

• If Tin ̸= ∅, return cert(qin,Ain)
• If Tin = ∅, do the following:

1. If qin has at most m vars., return cert(qin,Ain).

1. Otherwise, return the empty set.

The algorithm is clearly (p, ∅)-complete for each p ∈ Q, as it returns cert(p,Ain). It is, however, incomplete for q, which contains m+1 variables, as it returns the empty set regardless of Ain. Finally, ans is clearly sound, invariant under renamings (the way it operates does not depend on Ain, but rather on the shape of qin and Tin), and also monotonic.

The proof of Theorem 4 suggests that the notion of a wellbehaved algorithm is too general: no matter how large a QTB is, we can find a (rather unnatural) well-behaved algorithm that is complete for all queries in the QTB, but incomplete for some other queries. To obtain useful results, we thus need to require additional properties to CQ answering algorithms.

Towards this goal, we observe that most incomplete systems are based on database or RDF triple store technologies. Given O = T ∪A and q as input, these systems first deterministically "saturate" A with new assertions using the knowledge in T and then answer the query q directly w.r.t. the saturated ABox, as if it was a database. Hence, their behaviour can be characterised at a general level as given next.

Definition 5. An ABox-saturation algorithm for L is an algorithm that given as input an L-ontology O = T ∪ A and a CQ q proceeds as follows:

1. It computes a saturation ABox Af whose contents depend only on O, and such that A ⊆ Af .
2. It returns those answers to q w.r.t. Af containing only individuals from A. From now on, we abuse notation and write cert(q, Af ) to represent (only) such answers.

Furthermore, we assume that ans is stable: if Af is the saturation ABox for T ∪A, then the saturation ABox for T ∪Af is also Af .

Note that the negative result in Theorem 4 does not apply to the class of well-behaved ABox-saturation algorithms. Indeed, ABox-saturation algorithms are always complete if the TBox is empty. If one such algorithm is incomplete, it is because it fails to capture relevant knowledge from the TBox.

As shown in the following theorem, however, there exist TBoxes expressed in rather simple ontology languages for which no QTB exists, even if we restrict ourselves to wellbehaved ABox-saturation algorithms.

Theorem 6. There is a TBox T in L ∈ {EL,DL-Lite} such that no QTB exists for the class of all well-behaved ABoxsaturation algorithms for L.

Proof. (Sketch) Let Q be an arbitrary, but finite, set of CQs and let m be the maximum number of variables in a query fromQ. Consider the following EL-TBox

and the following query.

Similarly to the proof of Theorem 4, we can provide a wellbehaved ABox-saturation algorithm that is (p, Tel)-complete for each p ∈ Q, but not (q, Tel)-complete. Details are provided in our technical report. The proof for DL-Lite is analogous, by considering query q and the TBox Tlite = {A ⊑ ∃R.⊤, ∃R-.⊤ ⊑ A}, which entails Tel.

4 Computing a Query Testing Base

In this section we identify fairly general, yet practical, sufficient conditions on TBoxes that guarantee the existence of a QTB and yield algorithms to compute such a QTB efficiently.

Towards this goal, we observe that the proof of Theorem 6 exploits the fact that we can have DL TBoxes which imply cycles over existential quantifiers. As a result, no matter how large the maximum role depth of a query in the QTB is, we can always define an algorithm that "unfolds" the cycle only up to that depth. Such algorithmmay then be incomplete for queries with a larger role depth. Our intuition is that a QTB for T may be guaranteed to exist if we can ensure that such cycles do not occur (even implicitly) in T .

In Section 4.1 we focus on the logics DL-Lite and EL and provide a sufficient condition for preventing cycles. We assume from now onwards that EL TBoxes are normalised as described in the preliminaries.

In Section 4.2 we focus on the description logics underpinning the RL profile of OWL 2 [Motik et al., 2009], and show that for such DLs a QTB always exists.

4.1 DL-Lite and EL

To preclude cycles in DL-Lite and EL TBoxes, we rely on the weak acyclicity condition borrowed from database theory [Fagin et al., 2005] and which can be checked efficiently.

Roughly speaking, if O = T ∪A and T is weakly acyclic, then a run of the corresponding chase does not lead to an infinite generation of new individuals. Thus, weak acyclicity also prevents cyclic existential quantification.

The following definition is a straightforward application of the general notion of weak acyclicity to DL-Lite and EL.

Definition 7. Let T be an L-TBox, with L ∈ {DL-Lite, EL}. The dependency graph for T is the smallest graph with the following elements:

• Nodes: A node vA for each atomic concept A and nodes vR/1 and vR/2 for each atomic role in T .
• Edges: For R atomic and A,B either atomic or ⊤, let [A] = A, [∃R.B] = R/1 and [∃R-.B] = R/2.
• If T ∈ DL-Lite, then the graph contains the following edges for each positive GCI (B ⊑ C) ∈ T :
• ∗ An edge v[B] → v[C].
• ∗ A special edge v[B] ∗→ vR/2 if C = ∃R.⊤.
• ∗ A special edge v[B] ∗→ vR/1 if C = ∃R-.⊤.
• If T ∈ EL, it has edges vA → v⊤ and vR/1 → v⊤ for each atomic A and R, as well as the following edges for each ( ⊓ 1≤i≤n Bi ⊑ C) ∈ T with n ≤ 2:
• ∗ Edges v[Bi] → v[C].
• ∗ Special edges v[Bi] ∗→ v[D] and v[Bi] ∗→ v[R/2] if C = ∃R.D.

The dependency graph for T is weakly acyclic if it contains no cycle going through a special edge.

Intuitively, special edges signal the possible creation of a new individual via existential quantification during the chase construction, whereas the other edges keep track of possible propagation of information between existing individuals.

Example 8. Consider the following EL-TBox:

Although the dependency graph for T is cyclic, there is no cycle involving a special edge; hence, T is weakly acyclic.

The next theorem follows from a general result for weakly acyclic tuple-generating dependencies [Fagin et al., 2005].

Theorem 9. Let L ∈ {DL-Lite, EL} and let O = T ∪ A be a consistent L-ontology such that T is weakly acyclic. Then, there is a polynomial in the size of A bounding the length of every chase sequence. 3

Hence, weak acyclicity establishes a bound on the size of the chase (and hence also of the canonical model of O).

Since the chase is forest-shaped, each unnamed individual is connected to a named individual via a unique "path" of role assertions. Therefore, we can characterise the assertions generated by the application of chase rules as follows.

Definition 10. Let O = T ∪A be a consistent L-ontology for L ∈ {DL-Lite, EL}. A path of chaseL(O) is a subset of chaseL(O) of the form {A(a)} with A atomic, a named and A(a) ̸∈ A, or {ar(R1, a, b1), . . . , ar(Rn, bn-1, bn),B(bn)} with B either atomic or ⊤, a named and each bi unnamed.

We can then define a family of queries for checking whether an incomplete system captures the relevant information that could possibly be introduced by the application of chase rules. Such queries should depend only on the shape of the TBox T (and not on the particular input ABox).

Definition 11. Let L ∈ {DL-Lite, EL}, let T be an L-TBox with Tp ⊆ T the subset of T containing no negative GCIs, and let LHS = {C | C ⊑ D ∈ Tp}. For each C ∈ LHS, let c1 and c2 be individuals uniquely associated to C, and let

where A is either atomic or ⊤. Let AT = ⋃C∈LHS AC. A CQ q is a chase query w.r.t. T if it can be obtained from a path of chaseL(T ∪AT ) by replacing each individual c with a variable xc such that xc is distinguished iff c is named. 4

Example 12. The following are all the chase queries (modulo isomorphisms) w.r.t. TBox T from Example 8:

The following lemma shows that chase queries can be used to check for the presence of any relevant piece of new information introduced by the application of chase rules. 5

3 A chase sequence is any sequence of chase rule applications transforming A into chaseL(O).

4 Note that a chase query has exactly one distinguished variable.

5 A detailed proof can be found in our technical report.

Lemma 13. Let L ∈ {DL-Lite, EL} and let O be a consistent L-ontology. The CQ obtained by replacing in a path of chaseL(O) each (un)named individual c with an (un)distinguished variable xc is a chase query w.r.t. T .

As a result, if an ABox-saturation algorithm is complete for each chase query, it should be possible to homomorphically embed chaseL(O) into the saturation ABox Af computed by the algorithm for O. 5

Lemma 14. Let L ∈ {DL-Lite, EL} and let O = T ∪ A be a consistent L-ontology. Let ans be a well-behaved ABoxsaturation algorithm that is (q, T )-complete for each chase query q for T . Finally, let Af be the saturation ABox computed by ans for O. Then, there is a homomorphism μ from chaseL(O) to Af that maps named individuals to themselves.

Furthermore, weak acyclicity ensures the existence of a polynomial bound in both the size and number of chase queries for each input, as shown by the following Lemma.

Lemma 15. Let L ∈ {DL-Lite, EL}. Each chase query for a weakly acyclic L-TBox T is of size polynomial in the size of T . Also, there are polynomially many non-isomorphic chase queries in the size of T .

Proof. (Sketch) Given T and an ABoxA, Theorem9 implies that the the size of chaseL(O) is polynomial in the size of A. Let O′ = T ∪AT as in Definition 11. Since the size of AT is bounded by the size of T , the size of chaseL(O′ ) (and hence the size of each chase query) is polynomially bounded by the size of T . Finally, the number of chase queries is bounded by the number of assertions in chaseL(O′ ) and it is thus polynomially bounded by the size of T . 5

Lemmas 14 and 15 suggest that the set of chase queries for a weakly acyclic TBox T constitutes a QTB for T .

Theorem 16. Let L ∈ {DL-Lite, EL} and let T be a weakly acyclic L-TBox. Then, the set of all chase queries (unique up to isomorphism) is a QTB for T and the class of well-behaved ABox-saturation algorithms for L. Furthermore, the size of such QTB is polynomial in the size of T .

Proof. Let q be a CQ and let A be an ABox s.t. O = T ∪ A is consistent. Then, cert(q, O) = cert(q, chaseL(O)).

If c ∈ cert(q, chaseL(O)), there is a homomorphism σ from q to chaseL(O) which maps the distinguished variables to c. Since ans is (q′ , T )-complete for all chase queries q′ , Lemma 14 implies that there also exists a homomorphism μ between chaseL(O) and Af that maps named individuals to themselves. But then, σ composed with μ is a homomorphism from the variables of q to the individuals in Af which maps distinguished variables to c; hence, c ∈ cert(q,Af). Since ans(q,O) = cert(q,Af) we have that c ∈ ans(q,O), which implies that the set of all chase queries is a QTB. Finally, since T is weakly acyclic, Lemma 15 then implies that such QTB is of size polynomial in the size of T .

4.2 DLP

Description Logics Programs (DLP) [Grosof et al., 2003] is a prominent family of DLs which provide the logical underpinning for the RL profile of OWL 2 [Motik et al., 2009]. The logics in this family impose syntactic restrictions to avoid, on the one hand, the need to infer the existence of individuals not explicitly present in the ABox and, on the other hand, the need for nondeterministic reasoning. Such DLs have recently become popular since they are amenable to implementation using rule-based reasoning engines. In fact, many incomplete ontology reasoners use rule-based forward-chaining techniques to perform reasoning.

Therefore, DLP logics have been designed so as to satisfy the property given in the following lemma.

Lemma 17. Let L be in DLP. For each L-ontology O = T ∪ A, there is an ABox A′ mentioning only individuals from A and such that cert(q, O) = cert(q, A′ ) for every CQ q.

Since reasoning in DLP does not require the generation of "fresh" individuals, it is intuitive to expect that a QTB is guaranteed to exist. Furthermore, such QTB would only need to include queries asking for all instances of each atomic concept and each atomic role occurring in the ontology.

Theorem 18. Let L be in DLP and let T be a L-TBox. Let Q consist of a query qA(x) ← A(x) for each atomic concept A in T and a query qR(x, y) ← ar(R, x, y) for each (possibly inverse) role occurring in T . Then, Q is a QTB for T and the class of all well-behaved ABox-saturation algorithms.

Proof. Let ans be a well-behaved ABox-saturation algorithm that is (q′ , T )-complete for each q′ ∈ Q. Let q be a CQ and let A be an ABox such that O = T ∪ A is consistent. We show that cert(q, O) ⊆ ans(q, O).

If c ∈ cert(q,O), then c ∈ cert(q,A′ ), for some A′ as in Lemma 17. Hence, there is a homomorphism μ from q to A′ mapping distinguished variables to c and s.t. for each body atom A(t) (respectively R(t, t′ )) in q, A(μ(t)) ∈ A′ (respectively R(μ(t), μ(t′ )) ∈ A′ ); furthermore, μ(t) ∈ ans(qA, O) and 〈μ(t), μ(t′ )〉 ∈ ans(qR, O) since qA, qR ∈ Q and ans is complete for qA and qR. But then, μ(t) ∈ cert(qA,Af) and 〈μ(t), μ(t′ )〉 ∈ cert(qR,Af), with Af the saturation ABox for O computed by ans; thus, A(μ(t)) ∈ Af (respectively R(μ(t), μ(t′ )) ∈ Af ), and c ∈ ans(q, O), as required.

5 Evaluation

We have implemented a prototype query generator for DLLite and computed a QTB for a DL-Lite version of the LUBM TBox. The computation of LUBM's QTB required less than a second and contained only 16 queries, denoted as Q1-Q16. (Note that the QTB is so small because many concepts never appear on the right-hand side of a GCI).

We have used this QTB to evaluate the following systems: Sesame 2.3-prl, 6 OWLim, 7 Jena v2.6.4 8 using both its OntModel and InfModel interfaces, DLEJena, 9 Oracle's Semantic Data Store 10 using both the RDFS and OWLPrime profiles, and Pellet v2.2.2. 11 To this end, we generated the required datasets for each query in the QTB using the techniques from [Stoilos et al., 2010a], which we then used to compute the corresponding completeness degree for each system. (For DL-Lite TBoxes, a finite collection of such datasets is guaranteed to exist for each query [Stoilos et al., 2010a]).

6 http://www.openrdf.org/

7 http://www.ontotext.com/owlim/

8 http://jena.sourceforge.net/

9 http://lpis.csd.auth.gr/systems/DLEJena/

10 http://www.oracle.com/technetwork/database/options/semantictech/index.html

As expected, Pellet (a fully-fledged OWL 2 reasoner) was found to be complete for all queries. More interesting is the fact that Jena Full in its InfModel implementation was also complete for all queries and hence we can claim that it is indistinguishable from a complete reasoner like Pellet w.r.t. the LUBM TBox, regardless of the query and the data. In contrast, as shown in Table 1, all the other systems were found incomplete for some query.

We observe that all systems in Table 1 were incomplete for queries Q14-Q16, which involve undistinguished variables and hence require reasoning with existential quantifiers. Concerning the remaining queries, OWLim, Jena Micro in its OntModel implementation and Oracle OWLPrime, were found incomplete for Q11(x) ← Student(x). Even if Q11 contains only distinguished variables, LUBM's TBox entails the GCI GradStudent ⊑ Student, which can only be derived using existential quantifiers. In contrast, DLEJena is complete for Q11 since it pre-computes the ontology's subsumption hierarchy using a complete DL reasoner before saturating the ABox. Finally, Sesame and Oracle RDFS, which are essentially RDF-Schema reasoners, are additionally incomplete for all queries that require reasoning with constructs not available in RDFS, such as inverse roles.

6 Conclusions

In this paper, we have studied the problem of query generation for evaluating the completeness of Semantic Web reasoners. Our techniques allow us to formally determine whether an incomplete system is indistinguishable from a complete one for a given TBox, regardless of the data and the query. Our framework and algorithms are complementary to those in [Stoilos et al., 2010b] and [Stoilos et al., 2010a], in which both TBox and query were assumed to be fixed.

Our evaluation is, however, still preliminary and we are planning to implement and evaluate our query generation techniques also for EL. Finally, we are also planning to extend our techniques for more expressive DLs.

Acknowledgments

Research supported by the EU project SEALS (FP7-ICT238975). Bernardo Cuenca Grau is also supported by a Royal Society University Research Fellowship.

11 http://clarkparsia.com/pellet