We present a novel method of evaluating instance queries over description logic knowledge bases that derives from binary absorption. The method is designed to work well for large ABoxes and where the TBox is not necessarily Horn, e.g., where background knowledge requires the use of disjunction and negation. The method signi cantly improves the performance of instance checking, and particularly so in cases where a large number of concrete feature values are included. We also report on the results of a preliminary experimental evaluation that validates the e cacy of the method.
Two of the basic reasoning tasks over a DL knowledge base K = hT ; Ai are to determine if K is consistent, and so-called instance checking : to determine if a given concept assertion a : C (stating that individual a occurring in A belongs to concept C) is a logical consequence of a consistent K, written K j= a : C:
Usually, these tasks are combined in the sense that the latter is assumed to include the former. However, we believe that typical workloads for a reasoning service will include far more instance checking tasks than knowledge base consistency tasks. The resulting \separation of concerns" can therefore enable technology that is far more e cient for such workloads, particularly so in the case of non-Horn DL TBoxes T that preclude the possibility of computing so-called canonical ABoxes A0 from A (e.g., when disjunction is used in T ). We contribute to this development by introducing a novel adaptation of binary absorption for DL knowledge bases and demonstrate that the technique is e cacious for workloads that contain many thousands of instance checking tasks.
To date, work on absorption has focused on the concept satisfaction problem,
a simple case of the instance checking problem for knowledge bases with an ABox
consisting of a single assertion a : >. Indeed, it has been known for some time
in this case that lazy unfolding is an important optimization technique in model
building algorithms for satis ability [
To consider performance issues for instance checking in the context of
absorption, we rst consider how one can map instance checking problems to concept
satisfaction problems in which consistency is assumed, and then revisit
absorption in this new setting. In particular, we present an absorption generation
procedure that is an adaptation of an earlier procedure reported at the description
logics workshop [
Binary absorption combines two key ideas. The rst makes it possible to
avoid internalizing (at least some of the) terminological axioms of the form
(A1 u A2) v C, where the Ai denote primitive concepts and C a general concept.
The second is an idea relating to role absorptions developed by Tsarkov and
Horrocks [
A1 u (9R1 :A2) u (9R2:(A3 t A4)) v A5: In this case, the absorption would consist of a set of dependencies with a single primitive concept on the left-hand-side
fA2 v 8R1:A6; A3 v A7; A4 v A7; A7 v 8R2 :A8g and a second set of dependencies with a conjunction of two primitive concepts on the left-hand-side
f(A1 u A6) v A9; (A9 u A8) v A5g; in which A6, A7, A8 and A9 are fresh atomic concepts introduced by the binary absorption procedure. (Hereon, we refer to an instance of the latter set as a binary inclusion dependency.) A key insight and contribution of this paper is that it is not necessary for both concepts occurring in the left-hand-side of such a dependency to be atomic. In particular, we show that binary absorption raises the possibility of reducing assertion membership problems to concept satisfaction problems via the introduction of nominals in such dependencies, but without su ering the consequent overhead that doing so would almost certainly entail without binary absorption.
Note that there are other reasons that binary absorption is useful, beyond the well-documented advantages of reducing the need for internalization of general terminological axioms. In particular, it works very well for the parts of a terminology that are Horn-like, as illustrated by the above example.
Our contributions are as follows: 1. We introduce the notion of role and concrete feature guards in the context of a knowledge base for the DL dialect ALCIQ(D). In particular, we show how instance checking tasks in this dialect can map to concept satisfaction problems in the dialect ALCIOQ(D), but where binary absorption in combination with guards can usefully avoid reasoning about irrelevant ABox individuals and concrete facts with the assumption of knowledge base consistency. 2. We propose a generalization of binary absorption. In particular, we now allow nominals in place of one of the two left-hand-side concepts in an absorbed binary inclusion dependency. 3. We report on the results of an experimental evaluation that validates the e cacy of the proposed optimization.
After some preliminary de nitions, these contributions are the subject of
successive sections, and are followed in turn by our summary comments. Finally, note
that a short earlier version of this paper is being presented simultaneously in a
poster session of KR 2012 [
We consider instance checking problems in the context of knowledge bases expressed in terms of the DL dialect ALCIQ(D). However, such problems will be mapped to concept satisfaction problems in the more general dialect ALCIOQ(D). De nition 1 (Description Logic ALCIOQ(D)).
ALCIOQ(D) is a DL dialect based on disjoint in nite sets of atomic concepts NC, atomic roles NR, concrete features NF and nominals NI. Also, if A 2 NC, R 2 NR, a 2 NI, f; g 2 NF, n is a non-negative integer and C1 and C2 are concept descriptions, then A, :C1, C1 u C2, C1 t C2, >, n?R, 9:CR1:,Cf1,<8Rg:aCn1d, 9R :C1, 8R :C1, fag, 9 nR:C1, 9 nR:C1, 9 nR :C1, 9 f = k, where k is a nite string, are also concept descriptions.
An interpretation I is a pair I = ( I ] DI ; I ), where I is a non-empty set, DI a disjoint concrete domain of nite strings, and I is a function mapping each feature f to a total function f I : ! 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 I , NR to subsets of I I , and NI to elements of I . The interpretation is extended to compound descriptions in the standard way.
Concrete domain concepts such as f < k are considered to be a shorthand for (f < g) u (g = k), which, together with f = k, may be generalized as (t1 op t2), where t1 and t2 refer to either a concrete feature or a nite string, and op 2 f<; =g.
De nition 2 (TBox, ABox, and KB Satis ability). : A TBox T is a nite set of axioms of the form C1 v C2 or C1 = C2.: A TBox T is called primitive i it consists entirely of axioms of the form A = C with A 2 NC, each A 2 NC appears in at most one left hand side of an axiom, and T is acyclic. A 2 NC is de ned in T if T contains A v C or A =: C. An ABox A is a nite set of assertions of the form a : A, a : (f op k) and R(a; b).
Let K = (T ; A) be an ALCIOQ(D) knowledge base (KB). An interpretation I is a model of K, written I: j= T , i C1I C2I holds for each C1 v C2 2 T , C1I = C2I holds for each C1 = C2 2 T , aI 2 AI for a : A 2 A, (aI ; bI ) 2 RI , and f I (aI ) 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 CI 6= ;. 3
The absorption proceeds in two steps: rst guards that allow us to prune the exploration of the ABox during reasoning are added to the ABox assertions (in turn converted into TBox axioms about nominals) and then the resulting TBox is processed by an extended binary absorption algorithm. 3.1
In this section we convert an ALCIQ(D) knowledge base K to a TBox by representing individuals in K's ABox by nominals (i.e., in a controlled fragment of ALCIOQ(D)): De nition 3 (ABox Conversion). Let K = (T ; A) be a knowledge base. We de ne a TBox TA for the ABox of K:
TA = ffag u Defa v A j a : A 2 Ag [ ffag u Deff v (f op k) j a : (f op k) 2 Ag [ ffag u DefR v 9R:(fbg u Defb); fag u Defa v 9R:>;
fbg u DefR v 9R :(fag u Defa); fbg u Defb v 9R :> j R(a; b) 2 Ag Note that all the axioms resulting from ABox assertions are guarded by auxiliary primitive concepts of the form Def a, DefR, and Deff . Intuitively, these concepts, when coupled with an appropriate absorption allow a reasoner to ignore parts of the original ABox: all the constants for which Def a is not set, yielding considerable performance gains. For this idea to work we need to require (without loss of generality) that the TBox of K only uses quali ed at-most number restrictions of the form A v 9 nR:B where A and B are atomic concepts or their negations. Note that subsumptions of the form 9 nR:A v B are also considered to be at-most number restrictions and have to be equivalently rewritten in the above form and that nested restrictions must be unnested. It is easy to see that every ALCIQ(D) TBox can be transformed to an equi-satis able TBox that satis es this restriction by introducing new auxiliary concept names. Then we add the following assertions that manipulate the guards: De nition 4 (TBox Conversion). Let K = (T ; A) be a knowledge base. We de ne a TBox TT for the ABox of K as follows:
TT = fA v DefR; B v DefR j A v 9 nR:B 2 T g
[ f(t1 op t2) v Deff j f appears in t1 or in t2; (t1 op t2) appears in T g:
where D = Defa u(df appears in C Deff ).
Theorem 1. Let K = (T ; A) be a consistent knowledge base. Then
K j= a : C if and only if TK j= fag u D v C; Proof. Assume that there is an interpretation I0 that satis es TK such that (fag)I0 (D)I0 but (fag)I0 \ (C)I0 = ; and an interpretation I1 that satis es K in which all at-least restrictions are ful lled by anonymous objects. Hence, we do not need to consider at-least restrictions, no matter how expressed, in the construction below. Without loss of generality, we assume both I0 and I1 are treeshaped outside of the ABox (converted ABox). We construct an interpretation J for K [ fa : :Cg as follows: Let I0 be the set of objects o 2 I0 such that either o 2 (fag)I0 and (fag)I0 (Defa)I0 or o is an anonymous object in I0 rooted by such an object. Similarly let I1 be the set of objects o 2 I1 such that either o 2 (fag)I1 and (fag)I0 \ (Defa)I0 = ; or o is an anonymous object in I1 rooted by such an object. We set 1. J = I0 [ I1 ; 2. (a)J 2 (fag)I0 for (a)J 2 I0 and (a)J = (a)I1 for (a)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 (t1 op t2)); 4. (o1; o2) 2 (R)J if (a) (o1; o2) 2 RI0 and o1; o2 2 I0 , or (o1; o2) 2 RI1 and o1; o2 2 I1 ; or (b) o1 2 (fag)I0 \ (Defa)I0 , o2 2 (fbg)I1 and R(a; b) 2 A (or vice versa). We claim that (fag)J \ (C)J = ; (trivially) and J j= K: to show the latter part we only need to consider those R edges of the form covered by the last case (4b): the edges that cross between the two interpretations, i.e., when o1 2 (fag)I0 , o2 2 (fbg)I1 and R(a; b) 2 A. Now consider an inclusion dependency expressing an at-most restriction A v 9 nR:B 2 T . We can conclude that o1 62 (A)I0 as otherwise o1 2 (DefR)I0 by De nition 4 and thus o2 2 (Defb)I0 by De nition 3 which contradicts our assumption that (fbg)I0 \(Defb)I0 = ;. Hence the inclusion dependency is satis ed vacuously. The remaining edges, case (4a), satisfy all dependencies in K as the remainder of the interpretation J is copied from one of the two interpretations that satisfy K. 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 (Def a)I = (Deff )I = (DefR)I = I and (fag)I = faI g for all individuals a, concrete features f , and roles R. This extended interpretation then satis es TK and (fag)I (D)I \ (:C)I . 2 Also, in ALCI(D) we do not need to rely explicitly on the unique name assumption (UNA: the logic on its own cannot equate constants). However, we could allow explicit equalities and inequalities to the ABox and then preprocess them similarly to De nition 3, e.g., a b to fag u Defa v fbg u Defb and vice versa and so on. This is su cient for the construction of the interpretation J in the proof of Theorem 1 to go through. Note that the interpretations of constants (nominals) for which Def a is not set in I0 are irrelevant for constructing the interpretation J even though there could be assertions of the form > v C that are applicable to such objects (one could even augment all such assertions by adding guards to avoid this e ect). Therefore those constants (nominals) can be ignored completely by the reasoner and thus nodes corresponding to the constant symbols can be generated lazily on demand driven by the Def a concept. 3.2
Model building algorithms for checking the satisfaction of a concept C operate by manipulating an internal data structure (e.g., in the form of a node and edge labeled rooted tree with \back edges"). The data structure \encodes" a partial description of (eventual) interpretations I for which CI will be non-empty. Such a partial description will almost always abstract details on class membership for hypothetical elements of I and on details relating to the interpretation of roles. To talk formally about absorption and lazy evaluation, it is necessary to codify ffag; Ag fA1; A2g fag 2 LW (x) and fag 2 LW (y) implies x = y LW (x) , and (fag u A) v C 2 Tu implies C 2 LW (x) (x; y) 2 RI and 9R:> v C 2 Tu implies C 2 LW (x) (x; y) 2 RI and 9R :> v C 2 Tu implies C 2 LW (y)
LW (x) and (A1 u A2) v C 2 Tu implies C 2 LW (x)
A 2 LW (x) and A v C 2 Tu implies C 2 LW (x) :A 2 LW (x) and :A v C 2 Tu implies C 2 LW (x)
CCC111 v==:: CCC222 222 TTTggg iiimmmpppllliiieeesss ::CCC111ttt:CCC222 222 LLLWW ((xx))
W (x)
the idea of a partial description. This has been done in [
An interpretation I = ( I ; I ) is said to stem from W if I = W , I jNR = W , for each A 2 NC, A 2 LW (x) implies x 2 AI and :A 2 LW (x) implies x 2= AI , for each a 2 NI, fag 2 LW (x) implies x 2 fagI and :fag 2 LW (x) implies x 2= fagI , for each (f op k), (f op k) 2 LW (x) implies x 2 (f op k)I and :(f op k) 2 LW (x) implies x 2= (f op k)I .
A witness W is called admissible with respect to a TBox T if there is an interpretation I that stems from W with I j= T .
The properties satis ed by a witness have been captured by the original lemmas
2.6 and 2.7 in [
De nition 6. (Binary Absorption) Let K=fT ; Ag be a KB. A binary absorption of T is a pair of TBoxes (Tu; Tg) such that T Tu [ Tg and Tu contains axioms of the form A1 v C, :A1 v C, 9R:> v C (resp. 9R :> v C), and the form (A1 u A2) v C and (fag u A) v C, where fA; A1; A2g NC and a 2 NI.
A binary absorption (Tu; Tg) of T is called correct if it satis es the
following condition: For each witness W and x 2 W , if all conditions in Figure 1
are satis ed, then W is admissible w.r.t. T . A witness that satis es the above
property will be called unfolded.
1 The de nition of witness can be abstracted for any DLs that have ALCIO as a
sublanguage and that satisfy some criteria on the interpretations stated in [
In this section, we present a procedure for ABox absorption, which extends
binary absorptions [
The algorithm is given a TK that consists of arbitrary axioms. It proceeds by constructing
ve TBoxes Tg; Tprim; Tuinc;, Tbinc, and Trinc such that: T Tg [ Tprim [Tuinc [Tbinc [Trinc, Tprim is primitive, Tuinc consists of axioms of the form A1 v C, Tbinc consists of axioms of the form (A1 u A2) v C and (fag u A) v C and none of the above primitive concept are de ned in Tprim, and Trinc consists of axioms of the form 9R:> v C (or 9R :> v C). Here, Tuinc contains unary inclusion dependencies, Tbinc contains binary inclusion dependencies and Trinc contains domain and range inclusion dependencies.
In the rst phase, we move as many axioms as possible from T into Tprim. We initialize Tprim = ; and process each axiom X 2 T as follows.
: 1. If X is of the form A = C, A is not de ned in Tprim, and Tprim [ fXg is primitive, then move X to Tprim. 2. If X is of the form A =: C, then remove X from T and replace it with axioms
A v C and :A v :C: 3. Otherwise, leave X in T .
In the second phase, we process axioms in T , either by simplifying them or by placing absorbed components in Tuinc, Tbinc or Trinc. We place components that cannot be absorbed in Tg. We let G = fC1; : : : ; Cng represent the axiom > v (C1 t: : :tCn). Axioms are automatically converted to (out of) set notation. In addition, 8R:C (resp. 8R :C) is considered a shorthand for 9 0R::C (resp. 9 0R ::C).
(fA v C; :A v :C j A =: C 2 Tprimg [ Tuinc [ Tbinc [ Trinc; Tg): Otherwise, remove an axiom G from T . 2. Simplify G.
(a) If there is some :C 2 G such that C is not a primitive concept, then add (G [ NNF(:C) n f:Cg to T , where the function NNF( ) converts concepts to negation normal form. Return to Step 1. (b) If there is some C 2 G such that C is of the form (C1 u C2), then add both (G [ fC1g) n fCg and (G [ fC2g) n fCg to T . Return to Step 1. (c) If there is some C 2 G such that C is of the form C1 t C2, then apply associativity by adding (G[fC1; C2g)nfC1 tC2g to T . Return to Step 1. 3. Partially absorb G.
(a) If f:fag; :Ag G, and A is a guard, then do the following. If an axiom of the form ( a
f g u A) v A0 is in Tbinc, add G [ f:A0g n f:fag; :Ag to T . Otherwise, introduce a new concept A0 2 NC, add (G [ f:A0g) n f:fag; :Ag to T , and ( a
f g u A) v A0 to Tbinc. Return to Step 1. (b) If f:A1; :A2g G, and neither A1 nor A2 are de ned in Tprim, then do the following. If an axiom of the form (A1 u A2) v A0 is in Tbinc, add G [ f:A0g n f:A1; :A2g to T . Otherwise, introduce a new concept A0 2 NC, add (G [ f:A0g) n f:A1; :A2g to T , and (A1 u A2) v A0 to Tbinc. Return to Step 1. (c) If f8R:Cg = G (resp. f8R :Cg = G), then do the following. Add 9R :> v C (resp. 9R:> v C) to Trinc. Return to Step 1. (d) If 8R::A ( resp. 8R ::A) 2 G, then do the following. Introduce a new internal primitive concept A0 and add both A v 8R :A0 ( resp. A v 8R:A0) and (G [ f:A0g) n f8R::Ag (resp. nf8R ::Ag) to T . Return to Step 1. 4. Unfold G. If, for some A 2 G (resp. :A 2 G), there is an axiom A =: C in Tprim, then substitute A 2 G (resp. :A 2 G) with C (resp. :C), and add G to T . Return to Step 1. 5. Absorb G. If :A 2 G and A is not de ned in Tprim, add A v C to Tuinc where C is the disjunction of G n f:Ag. Return to Step 1. 6. If none of the above are possible (G cannot be absorbed), add G to Tg.
Return to Step 1.
Termination of our procedure can be established by a counting argument. Theorem 2. For any TBox T , the ABox absorption algorithm computes a correct absorption of T .
Proof. The proof is by induction on iterations of our algorithm. We abbreviate
the pair (fTprim [ Tuinc [ Tbinc [ Trinc; Tg [ T ) as T and claim that this pair is
always a correct binary absorption. Initially, Tuinc, Tbinc, Trinc and Tg are empty,
primitive axioms are in Tprim, and the remaining axioms are in T .
{ In Step 3(a) or Step 3(b), T is a correct absorption that derives from [
The correctness proof of this step follows from Lemma 4.3 and 4.4 in [
The proposed absorption technique has been implemented in our CARE Assertion Retrieval Engine (CARE) with an underlying ALCI(D) DL reasoner. The DL reasoner has no additional ABox reasoning optimizations other than the technique presented here, and it has implemented only axiom absorption and blocking for TBox reasoning. All experiments were conducted on a MacBook with a 2.4GHz Intel Duo processor and 4GB RAM. All times, given in seconds, were averaged out over three independent runs for all reasoners and a reasoning timeout (denoted {) is set to 1500 seconds. Queries were posed over a suite of datasets (KBs) describing digital cameras. The KBs consist of digital camera speci cations extracted from DPreview.com and pricing information from Amazon.com in which the seed KB, called DPC1, has one camera instance for each price found through Amazon for a camera model. The other KBs were generated from the seed KB by supplying n camera instances per price in DPCn. These KBs share the same TBox, i.e., 15 axioms, but have di erent ABox data, as shown in Figure 2a: it reports the number of individuals, concept, and role assertions, and the number of instances retrieved by each query over these datasets. Test queries are shown in Figure 3, which vary in query forms and selectivity.
Inds CAs RAs Q1 Q2 Q3 Q4
Q1 NG { PG 178.1 FG 6.5
Q2 Query response times in Figure 2b compare di erent guarding strategies. Speci cally, \No Guarding" (NG) is a straightforward implementation of the Tableaux algorithm (without assuming the consistency of the KB), \Partial Guarding" (PG) guards individuals so that only relevant individuals will be explored in Tableaux expansions, and \Full Guarding" (FG), in addition to \Partial Guarding," further guards feature concepts that describe objects in the data so that only query-relevant feature concepts participate in reasoning. Figure 2b shows that CARE timed out under the NG strategy, while it managed to answer all queries under the PG strategy and e ciency increased substantially under the DPC1 DPC3 DPC5 DPC7 DPC10
DPC1 DPC3 DPC5 DPC7 DPC10 (a) Query 1
(b) Query 2
DPC1 DPC3 DPC5 DPC7 DPC10
DPC1 DPC3 DPC5 DPC7 DPC10
(c) Query 3
(d) Query 4
FG strategy. As numerous other optimization techniques have been developed
(e.g., [
We show how, with the presumption that a knowledge base is consistent, one
can avoid considering irrelevant ABox individuals to the posed question while
preserving soundness and completeness of answers to instance checking tasks.
Our experiments show that in realistic situations arising, e.g., in
implementations of assertion retrieval [