Absorption for ABoxes with Local Universal Restrictions

Abstract

We elaborate on earlier work in which we developed a novel method for evaluating instance queries over DL knowledge bases that derives from binary absorption. An important feature of this earlier method and its re nement in this paper is that they avoid the need to check explicitly for consistency, a property that is desirable, for example, in SPARQL query evaluation over RDF data sets that can dynamically include sophisticated ontologies. In particular, we resolve a number of outstanding issues with the earlier method that limited its capabilities for knowledge bases that involve an extensive use of typing constraints expressed as axioms of the form A v 8R:B, or that require and use both role hierarchies and transitive roles. We also show how our more general method supports a safe use of nominals in instance queries, and how the method can therefore be used to evaluate basic graph patterns in the SPARQL query language. Finally, we present the results of a preliminary experimental evaluation that validates the e cacy of our more re ned method for instance checking.

-

In earlier work, we developed a novel method for instance checking over an ALCIQ(D) knowledge base [ 13, 14 ]. The method operated by reducing such problems to concept subsumption problems over an ALCIOQ(D) knowledge base. Roughly, this was achieved by introducing additional inclusion dependencies with nominals, and then by relying on a re nement of binary absorption [ 6 ] to ensure such dependencies are absorbed and thereby avoiding the overhead of reasoning about arbitrary ALCIOQ(D) terminologies that would otherwise be required.

This earlier method operates with the assumption that a knowledge base is consistent, and at no time requires any internal check to ensure this, for example, at the start of a session when the knowledge base is rst loaded. This enables very fast load times and is also a useful feature in cases where an agent must evaluate a SPARQL query over a knowledge base for which consistency has already been established by other agents or, indeed, for which such a test is simply infeasible.

In this paper, we present a more re ned version of this earlier method that addresses a number of outstanding issues that limited its e ectiveness. In particular, our new method can now accommodate arbitrary SHIQ(D) knowledge K norm bases with role hierarchies and transitive roles, and is also more adept in cases that involve a more extensive use of typing constraints, in particular for local universal restrictions such as inclusion dependencies of the form A v 8R:B. We also show how this new method supports a safe use of nominals in instance queries, and how the method can therefore be used to help reduce the cost of evaluating basic graph patterns (BGPs) in the SPARQL query language.

Like the earlier method, our new method proceeds in a series of steps that ultimately obtains an absorbed SHOIQ(D) terminology TK3 from an input SHIQ(D) knowledge base K = (T ; A), as illustrated in Figure 1: a normalized TBox T norm is rst obtained from T , essentially to extract embedded typing constraints, and then a series of three subsequent TBoxes TKi are derived from T norm and the ABox A. Our main result is that an instance check of the form K j= a : C then maps to a subsumption check

TK3 j= fag u D v C ; (1) where D is a concept that initializes an appropriate \ ring" of binary absorptions 3 in TK .

The rst and last steps in our new method are inherited unchanged from our earlier method [ 13 ], although we have included a more thorough presentation of T norm in Section 2 in which we give our preliminary de nitions. The remainder of the paper is organized as follows. Our primary contributions are in Section 3 in which we de ne the computation of TK1 and TK2 in Figure 1, and present our main result. We then show how nominals can safely occur in concept C in (1) above, that is, in a way that avoids any requirement for revising our method, and discuss how this can be useful in evaluating BGPs over SHIQ(D) knowledge bases. The results of a preliminary experimental evaluation of our new method are given in Section 4. These results are evidence that our new method is e cacious with respect to addressing the issues that were outstanding with the earlier version. Our review of related work and summary discussion then follow in Section 5. Part of this discussion relates to the two labelled arcs in Figure 1 in which we outline re nements to our method that can improve its performance or increase the scope of SHIQ(D) knowledge bases for which the method can be used.

Preliminaries We consider instance checking problems over knowledge bases expressed in terms of the DL dialect SHIQ(D), where D is the simple concrete domain of nite length strings. However, such problems will be mapped to subsumption checking problems in the more general logic SHOIQ(D) in which nominals can occur in inclusion dependencies. Although not really necessary, our de nition of SHOIQ(D) introduces a number of non-terminals in a concept grammar that helps to improve the clarity of the remainder of the paper.

De nition 1 (Description Logic SHOIQ(D)).

SHOIQ(D) is a DL dialect based on disjoint in nite sets of atomic concepts NC, atomic roles NR, concrete features NF and nominals NI. Let S 2 NR [ fR j R 2 NRg denote a general role. To avoid considering S , we de ne S = R if S = R and S = R otherwise. A role inclusion is in the form of S1 v S2. Let v be the transitive-re exive closure of v over the set fS1 v S2g [ fS1 v S2 j S1 v S2g, a role S is transitive, denoted Trans(S), i Trans(R) or Trans(R ) for some R where R v S and S v R. A role S is called complex if Trans(S0) for some S0 v S.

Let A 2 NC, a 2 NI, f; g 2 NF, and n be a non-negative integer, a SHOIQ(D) concept C is de ned as follows:

C

::= Cd ::= Cb ::= L ::=

Cd j C u C j C t C j fag j :fag j 9 nS:C1 j 9 Cb j f < g j f = k nS:C1 L j >

A j :A where k is a nite string. To avoid undecidability [ 5 ], a complex role S may occur only in concept descriptions of the form 9 0S:C1 or of the form 9 1S:C1.

An interpretation I is a pair I = (4I ] DI ; ( )I ), where 4I is a nonempty set, DI a disjoint concrete domain of nite strings, and ( )I is a function mapping each feature f to a total function (f )I : 4 ! D, the \=" symbol to the equality relation over D, the \<" symbol to the binary relation for an alphabetic ordering of D, a nite string k to itself, NC to subsets of 4I , NR to subsets of 4I 4I , and NI to singleton subsets of 4I , with the interpretation of inverse roles being (R )I = f(o2; o1) j (o1; o2) 2 RI g. The interpretation is extended to compound concepts in the standard way.

A TBox T is a nite set of constraints C of the form C1 v C2, S1 v S2 or Trans(S). An ABox A is a nite set of assertions of the form a : A, a : (f op k) and S(a; b). Let K = (T ; A) be an SHOIQ(D) knowledge base (KB). An interpretation I is a model of K, written I j= K, i (C1)I (C2)I holds for each C1 v C2 2 T , (S1)I (S2)I holds for each S1 v S2 2 T , f(o1; o2); (o2; o3)g (S)I implying (o1; o3) 2 (S)I holds for Trans(S) 2 T , (a)I 2 (A)I for a : A 2 A, ((a)I ; (b)I ) 2 (S)I for S(a; b) 2 A, (f )I ((a)I ) op k for a : (f op k) 2 A. A concept C is satis able with respect to a knowledge base K i there is an I such that I j= K and such that (C)I 6= ;.

By a slight abuse of grammar in the following, we allow simpler shorthand for more general concrete domain concepts Cd of the form (t1 op t2), where t1 and t2 refer to either a concrete feature or a nite string, and op 2 f<; ; >; ; =g. For example, f < k would be shorthand for (f < g) u (g = k), where g is a fresh concrete feature. Also, we write 8S:C (resp. 9S:C) as shorthand for the concept 9 0S::C (resp. 9 1S:C).

What we have called typing constraints in our introductory comments have the general form

Cb v 9 nS:Cb: As also discussed in our introductory comments, our initial mapping of a given SHIQ(D) knowledge base K requires that K adheres to a normalized form in which such constraints are always explicit.

De nition 2 (Normalized SHIQ(D) Terminologies). A SHIQ(D) constraint C is normalized if it has one of the forms Cb v 9 nS:Cb, CL v CR, S1 v S2, or Trans(S). where CL and CR are de ned by the following grammar.

CL ::= Cd j CL u CL j CL t CL j 9 nS:CL

CR ::= Cd j CR u CR j CR t CR j 9 nS:CR A SHIQ(D) terminology T is normalized if each constraint C occurring in T is normalized.

It is a straightforward process to obtain an equisatis able normalized terminology from an arbitrary SHIQ(D) terminology T . In particular, we write T norm to denote such a terminology, SC2T Cnorm, where Cnorm is obtained by an exhaustive top-to-bottom application of the following rules, where NNF(C) denotes concept C in negation normal form and also that A0 is always a fresh atomic concept.

(Cb v 9 nS:Cb)norm = fCb v 9 nS:Cbg (CL v CR)norm = fCL v CRg

(S1 v S2)norm = fS1 v S2g (Trans(S))norm = fTrans(S)g (Cb v C1 u C2)norm = (Cb v A0 u C1)norm [ (A0 v C2)norm (Cb v C1 t C2)norm = (Cb v A0 t C1)norm [ (A0 v C2)norm (Cb v 9 nS:C)norm = fCb v 9 nS:A0g [ (C v A0)norm (Cb v 9 nS:C)norm = fCb v 9 nS:A0g [ (A0 v C)norm

(C1 v C2)norm = (:A0 v NNF(:C1))norm [ (A0 v NNF(C2))norm Lemma 1. Let T be an arbitrary SHIQ(D) terminology. Then: (1) If I j= T norm for some I, then I j= T ; and (2) If I j= T for some I, then there is some interpretation I0 over the same domain such that I and I0 agree on the interpretation of all symbols in T and I0 j= T norm.

Proof. The proof follows by an induction on the normalization rules.

ABox Absorption for Local Universal Restrictions We now show how local universal restrictions of the form of L1 v 8S:L2 can be leveraged to further optimize ABox absorption. In our original ABox absorption framework [ 13, 14 ], the following pair of axioms are introduced for each S(a; b) occurring in A, and are then recognized as binary absorptions:

f(fag u GS) v 9S:(fbg u G); (fbg u GS ) v 9S :(fag u G)g: Intuitively, a tableau algorithm starts by generating the successor, the nominal on the right-hand side, after lazy unfolding. Other axioms are subsequently unfolded since the newly introduced nominal includes its guard, for example, the guard G for nominal f g

b . We now show how, under some circumstances, one can exploit local universal restrictions to eliminate guards for nominals on the right-hand side of such axioms, possibly replacing the above axioms with the pair

f(fag u GS) v 9S:fbg; (fbg u GS ) v 9S :fagg; and thereby avoiding subsequent unfolding. Again, Figure 1 illustrates this process. In particular: TK1 attempts such eliminations with simple syntactic checks in the original ABox, and TK2 uses TK1 for more general subsumption checks to do the same. Also observe that such eliminations are disallowed in the case that S is transitive. Details now follow.

Computing TK1: The computation of TK1 is based on our earlier method [ 13 ] from which we have extracted and re ned the de nitions of TT and TA to properly account for role hierarchies, for transitive roles and the above-mentioned syntactic guard elimination. In particular, TK1 is now given by

norm

T where each of the terminologies is de ned as follows: TT = f[L1ftv1 oGpSt;2Lv2vGfGjSf japLp1evars9 innSt1:Lo2r 2inTtn2o;rtm1gop t2 appears in T norm [ TT [ TA [ TF [ TF d [ TB [ TBd; g [ fGS2 v GS1 ; GS2 v GS1 j S1 v S2g [ f> v GS u GS j S appears in T norm and S is complexg TA = ffag u G v A j a : A 2 Ag [ ffag u Gf v f op k j a : (f op k) 2 Ag [ ffag u G v 9S:>; fbg u G v 9S :> j S(a; b) 2 Ag TF = ffag u GS v 9S:fbg j S(a; b) 2 A; Trans(S) 62 T norm and

for all L1 v 9 nS:L2 2 T norm : n = 0 and fa : L1; b : NNF(:L2)g \ A 6= ;g TF d = ffag u GS v 9S:(fbg u G) j S(a; b) 2 A and (Trans(S) 2 T norm or exists L1 v 9 nS:L2 2 T norm : n > 0 or fa : L1; b : NNF(:L2)g \ A = ;)g TB = ffbg u GS v 9S :fag j S(a; b) 2 A; Trans(S) 62 T norm and for all L1 v 9 nS:L2 2 T norm : n = 0 and fa : NNF(:L1); b : L2g \ A 6= ;g TBd = ffbg u GS v 9S :(fag u G) j S(a; b) 2 A and (Trans(S) 2 T norm or exists L1 v 9 nS:L2 2 T norm : n > 0 or fa : NNF(:L1); b : L2g \ A = ;)g Computing TK2: Recall that no reasoning is required in computing TK1. Instead, syntactic checks are performed for concept assertions of the form of a : L1 or b : L2 over the ABox. If these concept assertions are found, then it is guaranteed that S(a; b), together with the concept assertions, is consistent with any local universal restrictions of the form L1 v 8S:L2. Although such checks are far from complete, TK1 can now be used to perform subsumption checks to nd additional cases where local universal restrictions are satis ed by role assertions, that is, to 2 compute TK. The subsumption checks require the notion of a derivation concept (cf. Theorem 1) given by the following.

De nition 3 (Derivative Concept). The derivative concept DC for a general SHIQ(D) concept C is de ned as follows:

DC = 8 >> >><d Gfi if C = Cb; if C = (t1 op t2) and fi appears in t1 or t2; >DC1 u DC2 > >:GS u 8S:(DC1 u G) if C = C1 u C2 or C = C1 t C2; if C = 9 nS:C1 or C = 9 nS:C1:

TK2 is given by (TK1nT sub) [ T add, where T add and T sub are de ned as follows:

T sub = fC j C 2 TF d; C = \fag u GS v 9S:(fbg u G)"; Trans(S) 62 T norm and for all L1 v 9 nS:L2 2 T norm : n = 0 and

(TK1 j= fag u G v L1 or TK1 j= fbg u G v NNF(:L2))g [ fC j C 2 TBd; C = \fbg u GS v 9S :(fag u G)"; Trans(S) 62 T norm and for all L1 v 9 nS:L2 2 T norm : n = 0 and

(TK1 j= fag u G v NNF(:L1) or TK1 j= fbg u G v L2)g T add = ffag u GS v 9S:fbg j fag u GS v 9S:(fbg u G) 2 T sub g Instance checking as subsumption checking: Once TK2 is generated, it can be supplied to the absorption procedure (cf. [ 13 ]), which will produce the nal TBox TK3. Also, there is an important special case in which TK3 can be incrementally updated to accommodate new concept assertions of the form a : A in which A is not mentioned in TK3 (and therefore in the original SHIQ(D) knowledge base K): Lemma 2. Let K0 = K [ Sifai : Aig,where each Ai is an atomic concept not 3 occurring in TK. Then,

TK30 = TK [ 3 [ i

ffaig u Gai v Aig: Proof. The proof follows from the computation of TK1 and TK2 and the absorption procedure in [ 13 ].

Our main results now follow in which we show that an instance checking problem over a SHIQ(D) knowledge base K can be mapped to a subsumption checking problem over the SHOIQ(D) TBox TKi , for 1 i 3.

De nition 4. Let K = (T ; A) be a SHIQ(D) knowledge base and TK = TKi for any 1 i 3. Let a : C be an instance checking over K, and fag u D v C, be a subsumption check over TK, where D = G u DC . Let I0 be an interpretation that satis es TK such that (fag)I0 (D)I0 but (fag)I0 \ (C)I0 = ;; also, let I1 be an interpretation that satis es K in which all at-least restrictions are ful lled by ABox individuals and, if necessary, anonymous objects. Without loss of generality, we assume both I0 and I1 are tree-shaped outside of the ABox (converted ABox). De ne an interpretation J as follows: let a0 be any ABox individual and I0 be the set of objects o 2 4I0 such that either o 2 (fa0g)I0 and (fa0g)I0 (G)I0 or o is an anonymous object in 4I0 rooted by such an object. Similarly let I1 be the set of objects o 2 4I1 such that either o 2 (fa0g)I1 and (fa0g)I0 \ (G)I0 = ; or o is an anonymous object in 4I1 rooted by such an object. We set 1. 4J = I0 [ I1 ; 2. (a0)J 2 (fa0g)I0 for (a0)J 2 I0 and (a0)J = (a0)I1 for (a0)J 2 I1 ; 3. o 2 AJ if o 2 AI0 and o 2 I0 or if o 2 AI1 and o 2 I1 for an atomic concept A (similarly for concrete domain concepts of the form (t1op t2)); 4. (o1; o2) 2 (S)J if (a) (o1; o2) 2 SI0 and o1; o2 2 I0 , or (o1; o2) 2 SI1 and o1; o2 2 I1 ; or (b) o1 2 (fa0g)I0 \ (G)I0 , o2 2 (fb0g)I1 and S(a0; b0) 2 A (or vice versa); or (c) (o1; o2) 2 (S1)J and S1 v S; or (d) (o1; o0) 2 (S)J , (o0; o2) 2 (S)J and Trans(S) 2 T .

Lemma 3. For fo1; o2g 4J , if (o1; o2) 2 (S)J and Trans(S) 2 T , then either fo1; o2g I0 or fo1; o2g I1 , where I0, I0 , I1, I1 and J are given in De nition 4.

Proof. The proof proceeds by induction on all cases for interpretation of roles (i.e. 4th point) in De nition 4. Case (4a) is trivial; case (4b) is not applicable when Trans(S) 2 T as otherwise by the de nition of TT it holds that o1 2 (GS )I0 and thus the contradiction o2 2 (G)I0 . Case (4c) is trivial by the induction hypothesis if Trans(S1) 2 T . We show the case Trans(S1) 62 T is not applicable. Suppose o1 2 (fa0g)I0 \ (G)I0 and o2 2 (fb0g)I1 (or vice versa), then this is only possible through case (4b). While a similar contradiction can be drawn as in case (4b) because of GS v GS1 , i.e., o1 2 (GS1 )I0 and thus the contradiction o2 2 (G)I0 . Case (4d) follows from the induction hypotheses because either fo1; o2; o0g I0 or fo1; o2; o0g I1 hold. 2 Theorem 1. For any consistent SHIQ(D) knowledge base K, concept C, and individual a:

K j= a : C i

TK3 j= fag u G u DC v C: Proof (Outline). Since TK3 is obtained by an absorption of TK2, of which the correctness follows immediately from the proof of the absorption procedure in [ 13 ], it su ces to prove the case TK2, i.e., K j= a : C i TK2 j= fag u G u DC v C: Note that the case TK1 also follows from the case TK2. Consider De nition 4. We claim that (fag)J \ (C)J = ; (trivially) and J j= K. To show J j= K, note that the edges from case (4a) satisfy all dependencies in K as the remainder of the interpretation J is copied from I0 or I1. Thus, we only need to consider those S edges of the form covered by case (4b) (and the extended cases (4c) and (4d)): the edges that cross between the two interpretations, i.e., when o1 2 (fa0g)I0 , o2 2 (fb0g)I1 and S(a0; b0) 2 A. Now consider an inclusion dependency expressing an at-most restriction L1 v 9 nS:L2 2 T . There are two possibilities: in one case, we can conclude o1 62 (L1)I0 as otherwise o1 2 (GS )I0 by the de nition of TT 2 and thus o2 2 (G)I0 by the rules for construction of TK , which contradicts our assumption that (fb0g)I0 \(G)I0 = ;, hence the inclusion dependency is satis ed vacuously; in the other case, we cannot derive a contradiction because Gb0 was removed by our optimization shown in Sect. 3, then it must be the case that the axiom L1 v 9 0S:L2 2 T , i.e., L1 v 8S::L2, has been satis ed by the role assertion S(a; b). Lemma 3 stipulates that in case (4d) either fo1; o2; o0g I0 or fo1; o2; o0g I1 hold; hence any universal restriction of the form L1 v 8S:L2 (recall that concepts of the form 9 nS:L2 are disallowed for complex S) must be satis ed by (o1; o2) because it is already satis ed by (o1; o2) in I0 (I1, respectively). Edges from case (4c) are follows from all of the above. Hence all inclusion dependencies in K are satis ed by J .

The other direction of the proof follows by observing that if K [ fa : :Cg is satis able then the satisfying interpretation I can be extended to (Ga0 )I = (Gf )I = (GS )I = 4I for all individuals a0, concrete features f , and roles S, and (fa0g)I = faI0g. This extended interpretation then satis es TK2 and (fag)I (D)I \ (:C)I . 2 On a safe use of nominals: We brie y consider how nominals can participate in instance queries in such a way that answering the queries will not lead to complex reasoning for O. Such uses of nominals are considered safe because they do not require any modi cation to the underlying tableau procedure implemented for dialects without O. Note that a similar treatment of nominals has been given for E L dialects [ 7 ]. However, Lemma 4 shows that safe nominals can also be mentioned in instance queries for more expressive DL dialects. Lemma 4. For any SHIQ(D) knowledge base K, concept C and individual a, K j= a : C u l 9Si:faig i [fai : Aig j= a : C u l 9Si:Ai; (2) i i i where each Ai is a fresh atomic concept for each faig. We call any occurrence of a nominal in the left-hand-side instance query safe.

Proof. The proof is again tedious but straightforward.

Recall that Lemma 2 allows TK3 to be incrementally augmented if concept assertions of the form a : A need to be added to K (where A does not occur in TK3). Thus, in combination with Lemma 4, safe uses of nominals in instance queries a : C are easily supported by our method: one simply proceeds by temporarily adding binary absorptions of the form faig u Gai v Ai to TK3, and invoking the corresponding subsumption check for the right-hand-side of (2) on the result.

The utility of this capability for evaluating BGPs over SHIQ(D) knowledge bases is a simple consequence of the sometimes unavoidable need to do expensive instance checking [ 8 ], that is, when precomputed results by reasoning engines are insu cient for checking query results. Query classes for expensive instance checking can now include \links" to individuals in the range of partial bindings for query variables that are captured as safe uses of nominals in instance queries. 4

Experimental Results The absorption technique for local universal restrictions has been implemented in the CARE Assertion Retrieval Engine (CARE)1, which has an underlying SHI(D) DL reasoner. The DL reasoner features a limited number of optimizations, including the ABox absorption technique described in this paper, optimized double blocking [ 4 ], and dependency-directed backtracking [ 3 ]. Note that the set of nite strings is the only concrete domain supported by the reasoner.

All times are an average of ve independent runs on a single core of the 2.6GHz AMD Opteron 6282 SE processor of a Ubuntu 12.04 Linux server, with up to 4GB of memory. One of the two applications used in the experiments relates to digital cameras (DPC1). This ALCI KB consists of about 35 axioms, 18k individuals, and 25k role assertions. DPC1 has a considerable number of concrete feature concepts (around 70 features) for each model. Seven queries, varying in selectivity and complexity, were posed over DPC1, as listed in Table 1. The second application is based on the LUBM benchmark [ 1 ] using one university (LUBM0), which has about 17k individuals and 49k role assertions. Twelve queries out of the LUBM test queries2 were used (q2 and q9 were excluded since they are not expressible as instance queries). Since the experiments focus on instance retrieval, the selection conditions of the twelve queries were rei ed, e.g., q4 was rewritten as the instance query Professor u 9worksFor:A0, for some fresh atomic concept A0, and the concept assertion (http://www.Department0.University0.edu : A0) added to the original ABox (cf. Lemma 4).

The experimental results are shown in Figure 2 in which the execution time of CARE with/without our optimization has been compared. For DPC1, the preprocessing times (for ABox absorption) are about 7 seconds and 17 seconds when the optimization was o and on, respectively. In the latter case, about 16% of the role assertions were optimized for four universal restrictions (three of which are about the same role). Observe that q1 and q3 were improved by 45% and 14%, respecptively, while, for other queries, the runtime improvement was 1 http://code.google.com/p/care-engine/ 2 http://swat.cse.lehigh.edu/projects/lubm/queries-sparql.txt

Digital SLR mirrorless Compact Camera Digital SLR u (user review = \5:00")

Digital SLR u (:(user review = \5:00")) q5 9hasSale:(:(inventory status = \outOfStock")) q6 9hasManu:((manu name = \Kodak") t (9locatedIn:Europe Country))) q7 (9hasInstance :(Lens mount = \Nikon F mount")) u (9hasSale:9hasSeller:(seller name = \Walmart")) under 5%. The limited gains are not surprising in view of the proportion of role assertions optimized for local universal restrictions and of the characteristics of these queries (which were originally designed to deal with concrete features).

For LUBM0, the preprocessing times are 5 and 16 seconds when the optimization was o and on, respectively. With the optimization on, about 23% of the role assertions were optimized for six local universal restrictions. We have witnessed dramatic improvement with optimization on: all queries were improved by over 40%. In particular, q1 and q10 were improved by 90%. Most of the queries use the role (implicitly or explicitly) takesCourse that participates in the local universal restriction 8takesCourse:Course. Hence, the improvement is apparent. The experimental evaluation suggests that our optimization is most useful if there are many local universal restrictions, especially when di erent roles are involved, and that guard elimination strongly correlates with reduced query evaluation time.

We also observed that, for these KBs, syntactic checks in computing TK1 were not e cacious, that is, both TF and TB were empty. This is why computing TK2 required more time than the case when this optimization was o : a large 2 number of subsumption checks were performed during the computation of TK . In our summary comments, we outline how intermediate steps can be introduced to obtain TK2 in a way that, we believe, will greatly reduce the number of such subsumption checks at load time. 5

Related Work and Summary Instance queries are an important reasoning service over DL knowledge bases, and have been the subject of substantial work in the DL community. Although it is always possible to evaluate an instance query C(x) by performing a sequence of instance checks K j= a : C for each individual a occurring in K, reasoning engines usually try to reduce the number of such checks by using precomputed results or by \bulk processing" of a range of instance checks. An example of the latter is so-called binary retrieval [ 2 ], which is used to determine non-answers via a single (possibly large) satis ability check. There have been several approaches to exploiting precomputed results obtained at an earlier time: when a knowledge base is \loaded", or as a consequence of an explicit request [ 10 ]. Examples include the pseudo-model merging technique [ 2 ], presented earlier in [ 3 ] as a way to quickly falsify a subsumption check. In particular, a pseudo-model captures the deterministic consequences of concept membership for individuals. Note that model merging techniques are generally sound but incomplete. Methods on how precomputed information can be used to improve the e ciency of evaluating instance queries have also been developed [ 8, 10 ]. An approach to instance checking that has much in common with our own method was introduced in [ 12 ]. In this case, an ABox is partitioned into small islands such that an instance checking problem is routed to the island \owned" by an individual. Finally, although binary absorption is su cient to ensure any occurrences of our guard concepts are absorbed, more powerful absorption algorithms could also be used [ 9 ].

We have shown in earlier work how instance checking can be improved by introducing guards that in turn prune any unnecessary consideration of individuals and the (possibly large) number of facts about individuals [ 13, 14 ]. To recap, the method introduced in this earlier work assumes that knowledge bases are consistent and relies on a re nement of binary absorption to achieve e ciency. Our main result shows how the method can be re ned by an additional process that e ectively disables the introduction of \trigger" guards in binary absorptions, which in turn reduces the need for lazy unfolding.

There are two labelled arcs in Figure 1 that indicate where additional processing might be useful. In particular, the arc labelled \1" is where a process called nominal absorption can be applied that would allow our method to be used for SHOIQ(D) knowledge bases that admit a limited use of nominals [ 11 ]. The arc labelled \2" is where an intermediate process might be included to 1 eliminate guards by, say, reasoning about deterministic consequences using TK, which might considerably reduce the number of subsumption checks required in 2 computing TK.

References

[1] Yuanbo Guo , Zhengxiang Pan, and Je He in . LUBM: A benchmark for OWL knowledge base systems . Web Semant., 3 ( 2 -3): 158 { 182 , October 2005 .

[2] Volker Haarslev and Ralf Moller. On the scalability of description logic instance retrieval . J. Autom. Reason. , 41 ( 2 ): 99 { 142 , August 2008 .

[3] Ian Horrocks . Optimising Tableaux Decision Procedures For Description Logics . PhD thesis , the University of Manchester, 1997 .

[4] Ian Horrocks and Ulrike Sattler . Optimised reasoning for SHIQ . In ECAI'02 , pages 277 { 281 , 2002 .

[5] Ian Horrocks , Ulrike Sattler, and Stephan Tobies . Practical reasoning for expressive description logics . In Proceedings of the 6th International Conference on Logic Programming and Automated Reasoning, LPAR '99 , pages 161 { 180 , London, UK, UK, 1999 . Springer-Verlag.

[6] Alexander K. Hudek and Grant E. Weddell. Binary absorption in tableauxbased reasoning for description logics . In Description Logics'06 , 2006 .

[7] Yevgeny Kazakov , Markus Kroetzsch, and Frantisek Simancik . Practical reasoning with nominals in the E L family of description logics . In Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference, KR 2012 , 2012 .

[8] Ilianna Kollia and Birte Glimm . Cost based query ordering over OWL ontologies . In The Semantic Web - ISWC 2012 - 11th International Semantic Web Conference , Boston, MA, USA, November 11 - 15 , 2012 , Proceedings, Part I , pages 231 { 246 , 2012 .

[9] Boris Motik , Rob Shearer, and Ian Horrocks . Hypertableau reasoning for description logics . J. Artif. Intell. Res. (JAIR) , 36 : 165 { 228 , 2009 .

[10] Je rey Pound , David Toman, Grant E. Weddell , and Jiewen Wu . An assertion retrieval algebra for object queries over knowledge bases . In Toby Walsh, editor, IJCAI 2011, Proceedings of the 22nd International Joint Conference on Arti cial Intelligence , pages 1051 { 1056 , 2011 .

[11] Evren Sirin , Bernardo Cuenca Grau, and Bijan Parsia . From wine to water: Optimizing description logic reasoning for nominals . In Proceedings, Tenth International Conference on Principles of Knowledge Representation and Reasoning , pages 90 { 99 , 2006 .

[12] Sebastian Wandelt and Ralf Moller . Towards abox modularization of semiexpressive description logics . Applied Ontology , 7 ( 2 ): 133 { 167 , 2012 .

[13] Jiewen Wu , Alexander K. Hudek , David Toman, and Grant E. Weddell . Absorption for aboxes . In Proceedings of the 2012 International Workshop on Description Logics , DL- 2012 , 2012 .

[14] Jiewen Wu , Alexander K. Hudek , David Toman, and Grant E. Weddell. Assertion absorption in object queries over knowledge bases . In Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference, KR 2012 , 2012 .