=Paper=
{{Paper
|id=None
|storemode=property
|title=Absorption for ABoxes
|pdfUrl=https://ceur-ws.org/Vol-846/paper_34.pdf
|volume=Vol-846
|dblpUrl=https://dblp.org/rec/conf/dlog/WuHTW12
}}
==Absorption for ABoxes==
https://ceur-ws.org/Vol-846/paper_34.pdf
Absorption for ABoxes
Jiewen Wu, Alexander Hudek, David Toman, and Grant Weddell
Cheriton School of Computer Science
University of Waterloo, Canada
{j55wu, akhudek, david, gweddell}@uwaterloo.ca
Abstract. We present a novel method of evaluating instance queries
over description logic knowledge bases that derives from binary absorp-
tion. 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 significantly 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
efficacy of the method.
1 Introduction
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 |= 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 reason-
ing 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 efficient 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 efficacious for work-
loads 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 satisfiability [1]. It is also imperative for a large TBox to
be manipulated by an absorption generation procedure to maximize the benefits
of lazy unfolding in such algorithms, thereby reducing the combinatorial effects
of disjunction in underlying tableaux procedures [3].
To consider performance issues for instance checking in the context of absorp-
tion, we first consider how one can map instance checking problems to concept
satisfaction problems in which consistency is assumed, and then revisit absorp-
tion in this new setting. In particular, we present an absorption generation pro-
cedure that is an adaptation of an earlier procedure reported at the description
logics workshop [6]. This earlier procedure was called binary absorption and was
itself a generalization of the absorption theory and algorithms developed by Hor-
rocks and Tobies [4, 5]. The generalization makes it possible for lazy unfolding to
be used for parts of terminologies not handled by earlier absorption algorithms
and theory.
Binary absorption combines two key ideas. The first 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 [13]. To illustrate, binary absorption makes it possible to completely
absorb the inclusion dependency
A1 u (∃R1− .A2 ) u (∃R2 .(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
{A2 v ∀R1 .A6 , A3 v A7 , A4 v A7 , A7 v ∀R2− .A8 }
and a second set of dependencies with a conjunction of two primitive concepts
on the left-hand-side
{(A1 u A6 ) v A9 , (A9 u A8 ) v A5 },
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
suffering 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 gen-
eral 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 con-
text 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 satis-
faction 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
efficacy of the proposed optimization.
After some preliminary definitions, these contributions are the subject of succes-
sive 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 [14].
2 Preliminaries
We consider instance checking problems in the context of knowledge bases ex-
pressed 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).
Definition 1 (Description Logic ALCIOQ(D)).
ALCIOQ(D) is a DL dialect based on disjoint infinite sets of atomic concepts
NC, atomic roles NR, concrete features NF and nominals NI. Also, if A ∈ NC,
R ∈ NR, a ∈ NI, f, g ∈ NF, n is a non-negative integer and C1 and C2 are
concept descriptions, then A, ¬C1 , C1 u C2 , C1 t C2 , >, ⊥, ∃R.C1 , ∀R.C1 ,
∃R− .C1 , ∀R− .C1 , {a}, ∃≤n R.C1 , ∃≥n R.C1 , ∃≤n R− .C1 , ∃≥n R− .C1 , f < g and
f = k, where k is a finite string, are also concept descriptions.
An interpretation I is a pair I = (∆I ] DI , ·I ), where ∆I is a non-empty set,
D a disjoint concrete domain of finite strings, and ·I is a function mapping each
I
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 finite 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 finite string,
and op ∈ {<, =}.
Definition 2 (TBox, ABox, and KB Satisfiability).
.
A TBox T is a finite set of axioms of the form C1 v C2 or C1 = C2 . A TBox
.
T is called primitive iff it consists entirely of axioms of the form A = C with
A ∈ NC, each A ∈ NC appears in at most one left hand side of an axiom, and
.
T is acyclic. A ∈ NC is defined in T if T contains A v C or A = C. An ABox
A is a finite 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 |= T , iff C1I ⊆ C2I holds for each C1 v C2 ∈ T ,
.
C1I = C2I holds for each C1 = C2 ∈ T , aI ∈ AI for a : A ∈ A, (aI , bI ) ∈ RI ,
and f I (aI ) op k for a : (f op k) ∈ A. A concept C is satisfiable with respect
to a knowledge base K iff there is an I such that I |= K and such that C I 6= ∅.
3 On Absorbing an ABox
The absorption proceeds in two steps: first 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 Mapping Instance Checking to Subsumption Testing
In this section we convert an ALCIQ(D) knowledge base K to a TBox by rep-
resenting individuals in K’s ABox by nominals (i.e., in a controlled fragment of
ALCIOQ(D)):
Definition 3 (ABox Conversion). Let K = (T , A) be a knowledge base. We
define a TBox TA for the ABox of K:
TA = {{a} u Def a v A | a : A ∈ A}
∪ {{a} u Def f v (f op k) | a : (f op k) ∈ A}
∪ {{a} u Def R v ∃R.({b} u Def b ), {a} u Def a v ∃R.>,
{b} u Def R− v ∃R− .({a} u Def a ), {b} u Def b v ∃R− .> | R(a, b) ∈ A}
Note that all the axioms resulting from ABox assertions are guarded by auxiliary
primitive concepts of the form Def a , Def R , and Def f . 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 con-
siderable performance gains. For this idea to work we need to require (without
loss of generality) that the TBox of K only uses qualified at-most number re-
strictions of the form A v ∃≤n R.B where A and B are atomic concepts or their
negations. Note that subsumptions of the form ∃≥n R.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-satisfiable TBox that
satisfies this restriction by introducing new auxiliary concept names. Then we
add the following assertions that manipulate the guards:
Definition 4 (TBox Conversion). Let K = (T , A) be a knowledge base. We
define a TBox TT for the ABox of K as follows:
TT = {A v Def R , B v Def R− | A v ∃≤n R.B ∈ T }
∪ {(t1 op t2 ) v Def f | f appears in t1 or in t2 , (t1 op t2 ) appears in T }.
In the following we use TK for T ∪ TT ∪ TA .
Theorem 1. Let K = (T , A) be a consistent knowledge base. Then
K |= a : C if and only if TK |= {a} u D v C,
d
where D = Def a u( f appears in C Def f ).
Proof. Assume that there is an interpretation I0 that satisfies TK such that
({a})I0 ⊆ (D)I0 but ({a})I0 ∩ (C)I0 = ∅ and an interpretation I1 that satisfies
K in which all at-least restrictions are fulfilled 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 tree-
shaped outside of the ABox (converted ABox). We construct an interpretation
J for K ∪ {a : ¬C} as follows: Let Γ I0 be the set of objects o ∈ ∆I0 such that
either o ∈ ({a})I0 and ({a})I0 ⊆ (Def a )I0 or o is an anonymous object in ∆I0
rooted by such an object. Similarly let Γ I1 be the set of objects o ∈ ∆I1 such
that either o ∈ ({a})I1 and ({a})I0 ∩ (Def a )I0 = ∅ or o is an anonymous object
in ∆I1 rooted by such an object. We set
1. ∆J = Γ I0 ∪ Γ I1 ;
2. (a)J ∈ ({a})I0 for (a)J ∈ Γ I0 and (a)J = (a)I1 for (a)J ∈ Γ I1 ;
3. o ∈ AJ if o ∈ AI0 and o ∈ Γ I0 or if o ∈ AI1 and o ∈ Γ I1 for an atomic
concept A (similarly for concrete domain concepts of the form (t1 op t2 ));
4. (o1 , o2 ) ∈ (R)J if
(a) (o1 , o2 ) ∈ RI0 and o1 , o2 ∈ Γ I0 , or (o1 , o2 ) ∈ RI1 and o1 , o2 ∈ Γ I1 ; or
(b) o1 ∈ ({a})I0 ∩ (Def a )I0 , o2 ∈ ({b})I1 and R(a, b) ∈ A (or vice versa).
We claim that ({a})J ∩ (C)J = ∅ (trivially) and 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 ∈ ({a})I0 ,
o2 ∈ ({b})I1 and R(a, b) ∈ A. Now consider an inclusion dependency expressing
an at-most restriction A v ∃≤n R.B ∈ T . We can conclude that o1 6∈ (A)I0 as
otherwise o1 ∈ (Def R )I0 by Definition 4 and thus o2 ∈ (Def b )I0 by Definition 3
which contradicts our assumption that ({b})I0 ∩(Def b )I0 = ∅. Hence the inclusion
dependency is satisfied 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 satisfied by J.
The other direction of the proof follows by observing that if K ∪ {a : ¬C} is
satisfiable then the satisfying interpretation I can be extended to (Def a )I =
(Def f )I = (Def R )I = ∆I and ({a})I = {aI } for all individuals a, concrete
features f , and roles R. This extended interpretation then satisfies TK and
({a})I ⊆ (D)I ∩ (¬C)I . 2
Also, in ALCI(D) we do not need to rely explicitly on the unique name assump-
tion (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 Definition 3, e.g., a ≈ b to {a} u Def a v {b} u Def b and vice versa
and so on. This is sufficient 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 effect). 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 On Witnesses and Binary Absorption
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 C I 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
{a} ∈ LW (x) and {a} ∈ LW (y) implies x = y
{{a}, A} ⊆ LW (x) , and ({a} u A) v C ∈ Tu implies C ∈ LW (x)
(x, y) ∈ RI and ∃R.> v C ∈ Tu implies C ∈ LW (x)
(x, y) ∈ RI and ∃R− .> v C ∈ Tu implies C ∈ LW (y)
{A1 , A2 } ⊆ LW (x) and (A1 u A2 ) v C ∈ Tu implies C ∈ LW (x)
A ∈ LW (x) and A v C ∈ Tu implies C ∈ LW (x)
¬A ∈ LW (x) and ¬A v C ∈ Tu implies C ∈ LW (x)
C1 v C2 ∈ Tg implies ¬C1 t C2 ∈ LW (x)
.
C1 = C2 ∈ Tg implies ¬C1 t C2 ∈ LW (x)
.
C1 = C2 ∈ Tg implies C1 t ¬C2 ∈ LW (x)
Fig. 1: Absorption witness conditions
the idea of a partial description. This has been done in [5] by introducing the
notion of a witness, of an interpretation that stems from a witness, and of what
it means for a witness to be admissible with respect to a given terminology.
Definition 5. (Witness) Let C be an ALCIOQ(D) concept.1 A witness W =
(∆W , ·W , LW ) for C consists of a non-empty set ∆W , a function ·W that maps
NR to subsets of ∆W × ∆W , and a function LW that maps ∆W to sets of
ALCIOQ(D) concepts such that:
(W1) there is some x ∈ ∆W with C ∈ LW (x),
(W2) there is an interpretation I that stems from W, and
(W3) for each I that stems from W, x ∈ C I if C ∈ LW (x).
An interpretation I = (∆I , ·I ) is said to stem from W if ∆I = ∆W , ·I |NR =
· , for each A ∈ NC, A ∈ LW (x) implies x ∈ AI and ¬A ∈ LW (x) implies
W
x∈ / AI , for each a ∈ NI, {a} ∈ LW (x) implies x ∈ {a}I and ¬{a} ∈ LW (x)
implies x ∈/ {a}I , for each (f op k), (f op k) ∈ LW (x) implies x ∈ (f op k)I
and ¬(f op k) ∈ LW (x) implies x ∈ / (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 |= T .
The properties satisfied by a witness have been captured by the original lemmas
2.6 and 2.7 in [5]. We further extend binary absorption [6] to accommodate the
absorbed ABox as shown in Section 3.
Definition 6. (Binary Absorption) Let K={T , A} be a KB. A binary ab-
sorption 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, ∃R.> v C (resp. ∃R− .> v C), and the
form (A1 u A2 ) v C and ({a} u A) v C, where {A, A1 , A2 } ⊆ NC and a ∈ NI.
A binary absorption (Tu , Tg ) of T is called correct if it satisfies the follow-
ing condition: For each witness W and x ∈ ∆W , if all conditions in Figure 1
are satisfied, then W is admissible w.r.t. T . A witness that satisfies the above
property will be called unfolded.
1
The definition of witness can be abstracted for any DLs that have ALCIO as a
sublanguage and that satisfy some criteria on the interpretations stated in [5].
The distinguishing feature of our extension of binary absorption is the addition
of the first four implications in Figure 1. Binary absorption itself allows addi-
tional axioms in Tu to be dealt with in a deterministic manner, as illustrated
in our introductory example. ABox absorption, treating assertions as axioms,
extends binary absorption to handle nominals in binary inclusion dependencies.
In addition, domain and range constraints are also absorbed in a manner that
resembles role absorption introduced in [13].
4 A Procedure for Indirect ABox Absorption
In this section, we present a procedure for ABox absorption, which extends
binary absorptions [6]. Our algorithm also includes the possibility of absorb-
ing domain and range constraints. The procedure prioritizes binary absorption
to keep guarding constraints through restricted uses of nominals, yet it avoids
guards for domain and range axioms by employing a variant of role absorption,
The algorithm is given a TK that consists of arbitrary axioms. It proceeds by
constructing five 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 ({a} u A) v C
and none of the above primitive concept are defined in Tprim , and Trinc consists
of axioms of the form ∃R.> v C (or ∃R− .> v C). Here, Tuinc contains unary
inclusion dependencies, Tbinc contains binary inclusion dependencies and Trinc
contains domain and range inclusion dependencies.
In the first phase, we move as many axioms as possible from T into Tprim .
We initialize Tprim = ∅ and process each axiom X ∈ T as follows.
.
1. If X is of the form A = C, A is not defined in Tprim , and Tprim ∪ {X} 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 = {C1 , . . . , Cn } represent the axiom
> v (C1 t. . .tCn ). Axioms are automatically converted to (out of) set notation.
In addition, ∀R.C (resp. ∀R− .C) is considered a shorthand for ∃≤0 R.¬C (resp.
∃≤0 R− .¬C).
1. If T is empty, then return the binary absorption
.
({A v C, ¬A v ¬C | A = C ∈ Tprim } ∪ Tuinc ∪ Tbinc ∪ Trinc , Tg ).
Otherwise, remove an axiom G from T .
2. Simplify G.
(a) If there is some ¬C ∈ G such that C is not a primitive concept, then
add (G ∪ NNF(¬C) \ {¬C} to T , where the function NNF(·) converts
concepts to negation normal form. Return to Step 1.
(b) If there is some C ∈ G such that C is of the form (C1 u C2 ), then add
both (G ∪ {C1 }) \ {C} and (G ∪ {C2 }) \ {C} to T . Return to Step 1.
(c) If there is some C ∈ G such that C is of the form C1 t C2 , then apply
associativity by adding (G∪{C1 , C2 })\{C1 tC2 } to T . Return to Step 1.
3. Partially absorb G.
(a) If {¬{a}, ¬A} ⊂ G, and A is a guard, then do the following. If an axiom
of the form ({a} u A) v A0 is in Tbinc , add G ∪ {¬A0 } \ {¬{a}, ¬A} to
T . Otherwise, introduce a new concept A0 ∈ NC, add (G ∪ {¬A0 }) \
{¬{a}, ¬A} to T , and ({a} u A) v A0 to Tbinc . Return to Step 1.
(b) If {¬A1 , ¬A2 } ⊂ G, and neither A1 nor A2 are defined in Tprim , then
do the following. If an axiom of the form (A1 u A2 ) v A0 is in Tbinc ,
add G ∪ {¬A0 } \ {¬A1 , ¬A2 } to T . Otherwise, introduce a new concept
A0 ∈ NC, add (G ∪ {¬A0 }) \ {¬A1 , ¬A2 } to T , and (A1 u A2 ) v A0 to
Tbinc . Return to Step 1.
(c) If {∀R.C} = G (resp. {∀R− .C} = G), then do the following. Add
∃R− .> v C (resp. ∃R.> v C) to Trinc . Return to Step 1.
(d) If ∀R.¬A ( resp. ∀R− .¬A) ∈ G, then do the following. Introduce a new
internal primitive concept A0 and add both A v ∀R− .A0 ( resp. A v
∀R.A0 ) and (G ∪ {¬A0 }) \ {∀R.¬A} (resp. \{∀R− .¬A}) to T . Return to
Step 1.
.
4. Unfold G. If, for some A ∈ G (resp. ¬A ∈ G), there is an axiom A = C in
Tprim , then substitute A ∈ G (resp. ¬A ∈ G) with C (resp. ¬C), and add
G to T . Return to Step 1.
5. Absorb G. If ¬A ∈ G and A is not defined in Tprim , add A v C to Tuinc
where C is the disjunction of G \ {¬A}. 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 cor-
rect absorption of T .
Proof. The proof is by induction on iterations of our algorithm. We abbreviate
the pair ({Tprim ∪ 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 [6].
– In Step 3(c), T is a correct absorption for domain and range constraints.
The correctness proof of this step follows from Lemma 4.3 and 4.4 in [6].
– In Step 3(d), T is a correct absorption by [6].
– In any of Steps 1, 2, 5-8, T is a correct ABox absorption as they use only
equivalence preserving operations.
Thus, T is a correct binary absorption by induction.
5 Empirical Evaluation
The proposed absorption technique has been implemented in our CARE As-
sertion 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 Mac-
Book 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 digi-
tal camera specifications 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 different ABox data,
as shown in Figure 2a: it reports the number of individuals, concept, and role as-
sertions, 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
DPC1 5387 3225 7174 3 244 5 1426 Q1 Q2 Q3 Q4
DPC3 9711 3225 18672 9 732 11 1432 NG – – – –
DPC5 14035 3225 30170 15 1220 17 1438 PG 178.1 183.0 186.2 181.5
DPC7 18359 3225 41668 21 1708 23 1444 FG 6.5 6.0 6.1 6.1
DPC10 24845 3225 58915 30 2440 32 1453
(a) Description of KBs (b) Guarding Strategies (DPC1)
Fig. 2: Summary of results
Q1: ∃hasInstance− .(Digital SLR u (user review = “5.00”))
Q2: ∃hasInstance− .(Digital SLR u ¬(user review = “5.00”))
Q3: ∃hasInstance− .(Digital SLR u (user review = “5.00”)) t (price = “01400.00”)
Q4: ∃hasInstance− .(Digital SLR u (user review = “5.00”)) t ¬(price = “01400.00”)
Fig. 3: Test queries
Query response times in Figure 2b compare different guarding strategies. Specifi-
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 Guard-
ing,” 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 efficiency increased substantially under the
103
2
10
102
101
101
DPC1 DPC3 DPC5 DPC7 DPC10 DPC1 DPC3 DPC5 DPC7 DPC10
(a) Query 1 (b) Query 2
103
102
102
101 101
DPC1 DPC3 DPC5 DPC7 DPC10 DPC1 DPC3 DPC5 DPC7 DPC10
(c) Query 3 (d) Query 4
Fig. 1: Query response time comparison (logarithmic scale)
Fig. 4: Query response time comparison (logarithmic scale)
FG strategy. As numerous other optimization techniques have been developed
(e.g., [2]) and implemented in most state-of-the-art reasoners, we juxtaposed
their performance with CARE to show the efficacy of our proposed technique
for ABox reasoning. All queries were posed via OWL API 3 for Pellet 2.3.0 and
FaCT++ 1.5.3, and via JRacer in the form of nRQL for RacerPro 2.0. The
query response time in Figure 4 does not consider the loading or preprocessing
time for other reasoners, yet it includes the ABox absorption time (cf. Sect. 3)
for CARE. The results show that CARE outperformed all other reasoners in all
queries except Q1 (we believe this is due to deterministic precomputing at KB
load time). Given that CARE is not as optimized as other reasoners, the results
are significant.
6 Summary
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 implementa-
tions of assertion retrieval [11] in which a number of instance checking queries
are needed to answer a single user query, or in the case of ontology-based query
answering [9, 7, 12, 8], when non-Horn DLs are used (and thus the above tech-
niques cannot be applied), our technique makes querying often feasible. The
experiments show, on relatively simple examples, that, while using the proposed
technique allows answers to be computed in a few seconds, attempting the same
tasks without the optimization is infeasible. To be effective, the technique relies
on absorption procedures that have at least the capabilities of binary absorption.
An interesting avenue of further work would be to explore how highly optimized
DL reasoning procedures with more powerful capabilities for absorption such as
procedures based on hypertableau [10] could further improve performance.
References
1. Baader, F., Franconi, E., Hollunder, B., Nebel, B., Profitlich, H.J.: An empirical
analysis of optimization techniques for terminological representation systems, or:
Making KRIS get a move on. Applied Artificial Intelligence 4, 109–132 (1994)
2. Haarslev, V., Möller, R.: On the scalability of description logic instance retrieval.
J. Autom. Reason. 41(2), 99–142 (Aug 2008), http://dx.doi.org/10.1007/s10817-
008-9104-7
3. Horrocks, I.: Using an expressive description logic: FaCT or Fiction? In: KR’98.
pp. 636–647 (1998)
4. Horrocks, I., Tobies, S.: Optimisation of terminological reasoning. In: Description
Logics’00. pp. 183–192 (2000)
5. Horrocks, I., Tobies, S.: Reasoning with axioms: Theory and practice. In: KR’00.
pp. 285–296 (2000)
6. Hudek, A.K., Weddell, G.E.: Binary absorption in tableaux-based reasoning for
description logics. In: Description Logics’06 (2006)
7. Kontchakov, R., Lutz, C., Toman, D., Wolter, F., Zakharyaschev, M.: The com-
bined approach to query answering in DL-Lite. In: KR’10 (2010)
8. Kontchakov, R., Lutz, C., Toman, D., Wolter, F., Zakharyaschev, M.: The com-
bined approach to query answering in DL-Lite. In: IJCAI’11. pp. 2656–2661 (2011)
9. Lutz, C., Toman, D., Wolter, F.: Conjunctive query answering in the description
logic EL using a relational database system. In: IJCAI’09. pp. 2070–2075 (2009)
10. Motik, B., Shearer, R., Horrocks, I.: Hypertableau reasoning for description logics.
J. Artif. Intell. Res. (JAIR) 36, 165–228 (2009)
11. Pound, J., Toman, D., Weddell, G.E., Wu, J.: An assertion retrieval algebra for
object queries over knowledge bases. In: IJCAI’11. pp. 1051–1056 (2011)
12. Rosati, R., Almatelli, A.: Improving query answering over DL-Lite ontologies. In:
KR’10 (2010)
13. Tsarkov, D., Horrocks, I.: Efficient reasoning with range and domain constraints.
In: Description Logics’04 (2004)
14. Wu, J., Hudek, A., Toman, D., Weddell, G.: Assertion absorption in object queries
over knowledge bases. In: KR’12 (2012)