=Paper=
{{Paper
|id=None
|storemode=property
|title=Algebraic Reasoning for SHIQ
|pdfUrl=https://ceur-ws.org/Vol-846/paper_32.pdf
|volume=Vol-846
|dblpUrl=https://dblp.org/rec/conf/dlog/PourH12
}}
==Algebraic Reasoning for SHIQ==
https://ceur-ws.org/Vol-846/paper_32.pdf
Algebraic Reasoning for SHIQ
Laleh Roosta Pour and Volker Haarslev
Concordia University, Montreal, Quebec, Canada
Abstract. We present a hybrid tableau calculus for the description logic SHIQ
that decides ABox consistency and uses an algebraic approach for more informed
reasoning about qualified number restrictions (QNRs). Benefiting from integer
linear programming and several optimization techniques to deal with the interac-
tion of QNRs and inverse roles, our approach provides a more informed calculus.
A prototype reasoner based on the hybrid calculus has been implemented that de-
cides concept satisfiability for ALCHIQ. We provide a set of benchmarks that
demonstrate the effectiveness of our hybrid reasoner.
1 Introduction
It is well known that standard tableau calculi for reasoning with qualified number re-
strictions (QNRs) in description logics (DLs) have no explicit knowledge about set car-
dinalities implied by QNRs. This lack of information causes significant performance
degradations for DL reasoners if the numbers occurring in QNRs are increased. Over
the last years a family of hybrid tableau calculi has been developed that address this
inefficiency by integrating integer linear programming (ILP) with DL tableau methods,
where ILP is used to reason about these set cardinalities. We developed hybrid calculi
for the DLs ALCQ [3], SHQ [5], and SHOQ [4, 2]. In this paper we present a new
calculus that decides ABox consistency for the DL SHIQ, which extends SHQ with
inverse roles. This new calculus is a substantial extension of the one for SHQ [5] since
the interaction between inverse roles and QNRs results in back propagation of infor-
mation possibly adding new back-propagated QNRs, which, in turn, possibly require a
conservative extension of solutions obtained by using ILP.
Informally speaking this line of research is based on several principles: (i) role suc-
cessors are semantically partitioned into disjoint sets such that all members of one set
are indistinguishable w.r.t. to their restrictions; (ii) cardinalities of partitions are de-
noted by non-negative integer variables and the cardinality of a union of partitions can
be expressed by the sum of the corresponding partition variables; (iii) all members of
a non-empty partition are represented by a proxy element [6] associated with the cor-
responding partition variable; (iv) cardinality restrictions on a set of role successors
imposed by QNRs are encoded as a set of linear inequations; (v) the satisfiability of
a set of QNRs is mapped to the problem whether the corresponding system of linear
inequations has a non-negative integer solution and the involved proxy elements do not
lead to a logical contradiction. This approach is better informed than traditional tableau
methods because (i) (implied) set cardinalities are represented using ILP that is inde-
pendent of the values occurring in QNRs; (ii) the tableau part of the hybrid calculus
becomes more efficient because a set of indistinguishable role successors is represented
by one proxy; (iii) the partitioning of role successors supports semantic branching on
partition cardinalities and more refined dependency-directed backtracking.
2 Preliminaries
In this section we briefly describe syntax and semantics of SHIQ and its basic infer-
ences services. Furthermore, we define a rewriting that reduces SHIQ to SHIN \ in
order to apply the atomic decomposition technique [10], which is a basic foundation of
our calculus. Let NC be a set of concept names, NR a set of role names, NT R ⊆ NR
a set of transitive role names, NSR ⊆ NR a set of non-transitive role names with
NSR ∩ NT R = ∅. The set of roles is defined as NRS = NR ∪ {R− | R ∈ NR }. We de-
fine a function Inv such that Inv(R) = R− if R ∈ NR , and Inv(R) = S if R = S − .
For a set of roles RO = {R1 , . . . , Rn }, Inv(RO) = {Inv(R1 ), . . . , Inv(Rn )}. A
role hierarchy R is a set of axioms of the form R v S where R, S ∈ NRS and v∗
is transitive-reflexive closure of v over R ∪ {Inv(R) v Inv(S) | R v S ∈ R}. R is
called a sub-role of S and S a super-role of R if R v∗ S. A role R ∈ NSR is called
simple if R is neither transitive nor has a transitive sub-role. The set of SHIQ con-
cepts is the smallest set such that (i) every concept name is a concept, and (ii) if A is a
concept name, C and D are concepts, R is a role, S is a simple role, n, m ∈ N, n ≥ 1,
then C u D, C t D, ¬C, ∀R.C, ∃R.C, > nS.C, and 6 mS.C are also concepts. We
consider > (⊥) as abbreviations for A t ¬A (A u ¬A). A general concept inclusion
axiom (GCI) is an expression of the form C v D with C, D concepts. A SHIQ TBox
T w.r.t. a role hierarchy R is a set of GCIs.
Let I be a set of individual names. A SHIQ ABox A w.r.t. a role hierarchy R
.
is a finite set of assertions of the form of a : C, ha, bi : R, and a = 6 b with IA ⊆
I the set of individuals occurring in A and a, b ∈ IA and R a role. We assume an
interpretation I = (∆I , .I ), where the non-empty set ∆I is the domain of I and .I is
an interpretation function which maps each concept to a subset of ∆I and each role to
a subset of ∆I × ∆I . Semantics and syntax of the DL SHIQ are presented in [8].
An interpretation I holds for a role hierarchy R iff RI ⊆ S I for each R v S ∈ R.
An interpretation I satisfies a TBox T iff C I ⊆ DI for every GCI C v D ∈ T . An
interpretation I satisfies an ABox A if it satisfies T and R and all assertions in A such
.
that aI ∈ C I if a : C ∈ A, haI , bI i ∈ RI if ha, bi : R ∈ A, and aI 6= bI if a =
6 b ∈ A.
Such an interpretation is called a model of A. An ABox A is consistent iff there exists
a model I of A. A concept description C is satisfiable iff C I 6= ∅.
Let E be a concept expression, then clos(E) defines the usual closure of all con-
cept names occurring in E. Therefore, for a TBox T if C v D ∈ T , then clos(C) ⊆
clos(T ) and clos(D) ⊆ clos(T ). Likewise for an ABox A, if (a : C) ∈ A then
clos(C) ⊆ clos(A). Inspired by [10] we use a satisfiability-preserving rewriting to
replace QNRs with unqualified ones. This rewriting uses a new role-set difference op-
erator ∀(R \ R0 ).C for which (∀(R \ R0 ).C)I = {x | ∀y : hx, yi ∈ RI \ R0I implies
y ∈ C I }. We name the new language SHIN \ . We have (> nR)I = (> nR.>)I and
(6 nR)I = (6 nR.>)I . Considering ¬C ˙ as the standard negation normal form (NNF)
of ¬C we define a recursive function unQ which rewrites SHIQ concept descriptions
and assertions into SHIN \ .
Definition 1 (unQ). Let R0 be a new role in NR with R := R ∪ {R0 v R} for
each transformation. unQ rewrites the axioms as follows: unQ(C) := C if C ∈ NC ,
unQ(¬C) := ¬C if C ∈ NC otherwise unQ(¬C), ˙ unQ(∀R.C) := ∀R.unQ(C),
unQ(C u D) := unQ(C) u unQ(D), unQ(C t D) := unQ(C) t unQ(D),
P3
α(v001) = P1, α(v010) = P2, α(v100) = P4,
P1 P2
α(v011) = P3, α(v110) = P6, α(v101) = P5,
SR
S R α(v111) = P7
P7
P5 P6
ST R v001 + v011 + v101 + v111 6 2
ST RT
v010 + v011 + v110 + v111 > 1
P4
v100 + v110 + v101 + v111 6 2
T v100 + v110 + v101 + v111 > 3
Fig. 1. Atomic decomposition for 6 2S u > 1R u 6 2T u > 3T
unQ(> nR.C) := > nR0 u ∀R0 .unQ(C), unQ(6 nR.C) := 6 nR0 u ∀(R \ R0 ).
unQ(¬C),˙ unQ(a : C) := a : unQ(C), unQ(ha, bi : R) := ha, bi : R,
. .
unQ(a = 6 b) := a =6 b.
Note that this rewriting generates a unique new role for each QNR. For instance,
unQ(> nR.C u 6 mR.C u > kR− .D) is rewritten to > nR1 u ∀R1 .C u 6 mR2 u
∀(R \ R2 ).¬C u > kR3 u ∀R3 .D and {R1 v R, R2 v R, R3 v R− } ⊆ R. SHIN \
is not closed under negation due to the fact that unQ(6 nR.C) itself creates a nega-
tion which must be in NNF before further applying unQ. In order to avoid the whole
negating problem for the concept description generated by unQ(6 nR.C) and unQ(>
nR.C) the calculus makes sure that the application of unQ starts from the innermost
part of an axiom, therefore such concept descriptions will never be negated.
Atomic decomposition A so-called atomic decomposition for reasoning about sets was
proposed in [10] and later applied to DLs for reasoning about sets of role fillers (see
Def. 3 for role fillers). For instance, for the concept description 6 2S u > 1R u 6 2T u
> 3T we get 7 disjoint partitions shown in the left part of Fig. 1, where partition P1
represents S-fillers that are neither R nor T fillers and P5 represents fillers in the in-
tersection of S and T that are not R-fillers, etc. For example, due to the disjointness of
Pi , 1 ≤ i ≤ 7, the cardinality of all S-fillers can be expressed as |P1 |+|P3 |+|P5 |+|P7 |
(| · | denotes the cardinality of a set). The satisfiability of the above-mentioned concept
descriptions can now be defined by finding a non-negative integer solution for the in-
equations shown at the bottom-right part of Fig. 1, where vi denotes the cardinality of
Pi with i in unary encoding.
3 SHIQ ABox Calculus
In this section we introduce our calculus and the tableau completion rules for SHIQ.
Definition 2 (Completion forest). The algorithm generates a model consisting of a set
of arbitrarily connected individuals in IA as the roots of completion trees. Ignoring the
connections between roots, the created model is a forest F = (V, E, L, LE , LI ) for a
SHIQ ABox A. Every node Px ∈ V is labeled by L(x) ⊆ clos(A) and LE (x) as a set
of inequations of the form i∈N vi ./ n with n ∈ N and ./ ∈ {>, 6} and variables
vi ∈ V. Each edge hx, yi ∈ E is labeled by the set L(hx, yi) ⊆ NR . For each node
x, LI (x) is defined to keep an implied back edge for x equivalent to Inv(L(hy, xi)),
where y is a parent of x (see Def. 4). For the nodes with no parents (root nodes) LI will
be the empty set.
Definition 3 (-successor, -predecessor, -neighbour, -filler). Given a completion tree,
for nodes x and y with R ∈ L(hx, yi) and R v∗ S, y is called S-successor of x and
x is Inv(S)-predecessor of y. If y is an S-successor or an Inv(S)-predecessor of x
then y is called and S-neighbor of x. In addition, if R ∈ L(hx, yi) then y is an R-filler
(role-filler) for x. The R-fillers of x are defined as F il(x, R) = {y | hxI , y I i ∈ RI }.
Definition 4 (Precedence). Due to the existence of inverse roles for each pair of indi-
viduals x, y, R ∈ L(hx, yi) imposes Inv(R) ∈ L(hy, xi). A global counter PR keeps
the number of nodes and is increased by one when a new node x is created, setting
PR x = PR. Hence, each node is ranked with a PR. A successor of x with the lowest
PR is called parent (parent successor) of x and others are called its children. Accord-
ingly, a node x has a lower precedence than a node y if x has a lower rank compared
to y. Also, each node has a unique rank and no two nodes have the same rank.
Definition 5 (ξ). Assuming a set of variables V, a unique variable v ∈ V is associated
with a set of role names RV v . Let V R = {v ∈ V | R ∈ RV v } be the set of all variables
which are related to a rolePR. The function ξ maps number restrictions to inequations
such that ξ(R, ./,n) := ( vi ∈V R vi ) ./ n.
Definition 6 (Distinct partitions). Rx is defined as the set of related roles for x such
that Rx =S{S | {ξ(S, >,n), ξ(S, 6,m)} ∩ LE (x) 6= ∅}. A partitioning Px is defined
as Px = P ⊆Rx {P } \ {∅}. For a partition Px ∈ Px , PxI = ( S∈Px F ilI (x, S)) \
T
( S∈(Rx \Px ) F ilI (x, S)) with F ilI (x, S) = {y I | y ∈ F il(x, S)}. Let α be a mapping
S
α : V ↔ Px for a node x, each variable v ∈ V is assigned to a partition Px ∈ Px such
that α(v) = Px .
The definition clearly demonstrates that the fillers of x related to the roles of partition
Px are not the fillers of the roles in Rx \ P (other partitions). Therefore, by definition
the fillers of x associated with the partitions in Px are mutually disjoint w.r.t. the inter-
pretation I. An arithmetic solution is defined using the function σ : V → N mapping
each variable in V to a non-negative integer. Let Vx be the set of all variables assigned
to a node x such that Vx = {vi ∈ V | vi ∈ LE (x)}, a solution Ω for a node x is
Ω(x) := {σ(v) = n | n ∈ N, v ∈ Vx }. The inequation solver uses an objective func-
tion to determine whether to minimize the solution or maximize it. We minimize the
solution in order to keep the size of the forest small.
The example in Fig. 1 depicts the process of finding an arithmetic solution in more
detail. Let L(x) = {6 2S, > 1R, 6 2T , > 3T } be the label of node x. Applying the
atomic decomposition for the related roles Rx = {S, R, T } results in seven disjoint
partitions such that Px = {Pi | 1 6 i 6 7} where P1 = {S}, P2 = {R}, P4 = {T },
P3 = {S, R}, P5 = {S, T }, P6 = {R, T }, P7 = {R, S, T } as shown in Fig. 1. In order
to simplify the mapping between variables and partitions, each bit in the binary coding
of a variable index represents a specific role in Rx . Therefore, in this example the first
bit from right represents S, the second R, and the last T . Since |Rx | = 3, the number of
variables in Vx becomes 23 − 1. The mapping of variables and the resulting inequations
in LE (x) are also shown in Fig. 1.
Definition 7 (Node Cardinality). The cardinality associated with proxy nodes is de-
fined by the mapping card : V → N.
Since the hybrid algorithm requires to have all numerical restrictions encoded as a set of
inequations, three functions are defined to map number restrictions (NRs) to inequations
and/or further constrain variables. Function ξ (see Def. 5) is used in the >-Rule and 6-
Rule as shown in Fig. 2. Function ζ and ς also add new inequations to the label LE
of a node and modify the variables. The functions ζ and ς are respectively used in the
IBE-Rule and resetIBE -Rule as shown in Fig. 2.
Definition 8 (ζ). For a set of roles RO and k ∈ N, the function ζ(RO, k) maps number
restrictions to inequations via the function ξ for each Rj ∈ RO. ζ(RO, k) returns a set
of inequations such that ζ(RO, k) = {ξ(Rj , >, k) | Rj ∈ RO} ∪ {ξ(Rj , 6, k) | Rj ∈
RO}. For v ∈ V Rj , if Rj ∈ α(v) ∧ α(v) * RO then v 6 0 is also returned.
Definition 9 (ς). For a set of roles RO and k ∈ N, the function ς(RO, k) maps number
restrictions to inequations via the function ξ for each Rj ∈ RO. ς(RO, k) returns a set
of inequations such that ς(RO, k) = {ξ(Rj , >, k) | Rj ∈ RO} ∪ {ξ(Rj , 6, k) | Rj ∈
RO}. For v ∈ V Rj , if RO = α(v) then v = k is also returned.
Definition 10 (Proper Sub-Role). For each role in existing number restrictions a set
will be assigned which contains a specific type of sub-role called proper sub-role. A
proper sub-role <(R) for a role R is defined as <(R) = {Ri | (R ∈ NR ∪ Inv(R)) ∧
Ri v R}.
This makes specializing the edges between nodes possible. Therefore, in our algorithm
when a role set is assigned to L(hx, yi) a new proper sub-role Si will be created for
each role S ∈ L(hx, yi), where <(S) = <(S) ∪ {Si }, and will be assigned to the edge
label. A role in <(S) cannot have any proper sub-role. Only roles that occur in number
restrictions and their inverses can have proper sub-roles. Since these proper sub-roles
do not appear in the logical label of nodes, they do not violate the correctness of our
algorithm.
Definition 11 (Blocked Node). Since SHIQ does not have the finite model property
pair-wise blocking [7] is used. Node y is blocked by node x, also called witness,
if L(x) = L(y) and for their successors y 0 , x0 , L(y 0 ) = L(x0 ) and L(hx, x0 i) =
L(hy, y 0 i). Also, unreachable nodes which were discarded from the forest (due to the
application of the reset-Rule or resetIBE -Rule) are called blocked. In order to detect
blocked nodes, all roles in a proper sub-role of role R are considered equivalent to R.
Definition 12 (Clash Triggers). A node x contains a clash if {A, ¬A} ⊆ L(x) (logical
clash) or LE (x) does not have a non-negative integer solution (arithmetic clash).
The interaction between the tableau rules and the inequation solver is similar to the clash
triggers. No particular rule is needed to invoke the inequation solver. For each LE (x),
there is always a solution (if there exists any) otherwise a clash occurs. If a variable
changes or LE (x) is extended, a new solution will be calculated automatically. The
completion rules for a SHIQ ABox are shown in Fig. 2, listed in decreasing priority
from top to bottom. Rules in the same cell have the same priority. Rules with lower
priorities cannot be applied to a node x, which is not blocked, if there exists any rule
with a higher priority still applicable to it. Among the completion rules in Fig. 2, the u-
Rule, t-Rule, ∀-Rule, ∀+ -Rule are the same as in standard tableaux. The merge-Rule,
∀\ -Rule, ch-Rule, >-Rule, 6-Rule are similar to [5].
>-Rule and 6-Rule: all number restrictions from L(x) are collected via these two
rules. The function ξ maps them to inequations according to the proper atomic decom-
position and adds them to LE (x).
IBE-Rule: this rule considers the implied back edge as a set of NRs, maps them to
a set of inequations, add the inequations to the LE , and determines potential variables
that can represent the IBE through elimination of the non-related variables. Assume that
for a node x a successor y has been created with L(hx, yi). This implies a back edge for
reset-Rule if {(≤ nR), (≥ nR)} ∩ L(x) 6= ∅ and ∀v ∈ Vx : R ∈ / α(v)
then set LE (x) := ∅ and
for every successor y of x set L(hx, yi) := ∅ and,
if y in not parent of x set L(hy, xi) := ∅
resetIBE -Rule if Inv(R) ∈ L(hy, xi) but R ∈ / L(hx, yi)
then set LE (x) := LE (x) ∪ {ζ(L(hx, yi), card(y))} and,
for every successor y of x set L(hx, yi) := ∅ and,
if y is not parent of x set L(hy, xi) := ∅
merge-Rule if there exist root nodes za , zb , zc for a, b, c ∈ IA such that
R0 v∗ Rab , R0 ∈ L(hza , zc i)
then merge the node zb , zc and their labels and,
replace every occurrence of zb in the completion graph by zc
u-Rule if (C1 u C2 ) ∈ L(x) and {C1 , C2 } * L(x)
then set L(x) = L(x) ∪ {C1 , C2 }
t-Rule if (C1 t C2 ) ∈ L(x) and {C1 , C2 } ∩ L(x) = ∅
then set L(x) = L(x) ∪ {X} for some X ∈ {C1 , C2 }
∀-Rule if ∀S.C ∈ L(x) and there is an S-neighbour y of x with C ∈ / L(y)
then set L(y) = L(y) ∪ {C}
∀\ -Rule if ∀R \ S.C ∈ L(x) and there is an R-neighbour y of x with C ∈ / L(y)
and y is not S-neighbour of x
then set L(y) = L(y) ∪ {C}
∀+ -Rule if ∀S.C ∈ L(x) and there is some R with T rans(R) and R v∗ S
and there is R-neighbour y of x with ∀R.C ∈ / L(y)
then set L(y) = L(y) ∪ {∀R.C}
ch-Rule if there occurs v in LE (x) with {v ≥ 1, v ≤ 0} ∩ LE (x) = ∅
then set L(x) = L(x) ∪ {X} for some X ∈ {v ≥ 1, v ≤ 0}
≥-Rule if (≥ nR) ∈ L(x) and ξ(R, ≥, n) ∈ / LE (x)
then set LE (x) = LE (x) ∪ {ξ(R, ≥, n)}
≤-Rule if (≤ nR) ∈ L(x) and ξ(R, ≤, n) ∈ / LE (x)
then set LE (x) = LE (x) ∪ {ξ(R, ≤, n)}
IBE-Rule if LI (x) 6= ∅ and {ς(LI (x), 1)} ∩ LE (x) = ∅
then set LE (x) = LE (x) ∪ {ς(LI (x), 1)}
BE-Rule if there exists v occurring in LE (x) such that σ(v) = 1, R ∈ α(v),
R ∈ LI (x) and y is parent of x with L(hx, yi) = ∅
then set L(hx, yi) := α(v)
RE-Rule if there exists v occurring in LE (za )
such that σ(v) = 1, za , zb root nodes,
Rab ∈ α(v) with x, b ∈ IA and L(hza , zb i) = ∅
then set L(hza , zb i) := α(v), LI (zb ) := Inv(α(v))
f il-Rule if there exists v occurring in LE (x)
such that σ(v) = n with n > 0,
x is not blocked and ¬∃y : L(hx, yi) = α(v)
then create a new node y and set L(hx, yi) := α(v),
LI (y) := Inv(α(v)) and card(y) = n
Fig. 2. The complete tableaux expansion rules for SHIQ-ABox
y with a label LI (y) = Inv(L(hx, yi)). This back edge is considered as a set of NRs
of the form > 1Ri , 6 1Ri where Ri ∈ Inv(L(hx, yi)). The IBE-Rule P transforms the
implied back edge into a set of inequations in LE (y) of the form ( vj ∈V Ri vj ) > 1
and ( vj ∈V Ri vj ) 6 1 using the function ς. Since the inequations representing the back
P
edge are restricted to the value one, only one common variable vk in these inequations
will be σ(vk ) = 1. In addition, ς ensures that the potential variables for IBE include all
the roles in LI (y) (see Def. 9).
resetIBE -Rule: this rule extends LE as follows. If for a node y and its parent node
x, L(hx, yi) 6= Inv(L(hy, xi)), then it implies that a new role should be considered in
LE (x) due to the restrictions of its child y. Therefore, the resetIBE -Rule fires for x
where ζ extends LE (x) to consider Inv(L(hy, xi)) and ensures that the specific vari-
able representing it is included in the solution as in Def. 8.
reset-Rule: if a new number restriction with a new role R is added to the logical
label of a node x, all its children are discarded from the tree and LE (x) = ∅.
BE-Rule: this rule fills a label of the back edge a node to its parent due to the
solution of the inequation solver. If a variable v in a solution exists such that σ(v) = 1
and LI (y) ⊆ α(v), then v represents the back edge and the BE-Rule fires and fills the
edge label.
We adjust the edges between a pair of nodes to satisfy the nature of the inverse roles
between them. Interactions of IBE-Rule, BE-Rule, and resetIBE -Rule maintain this
characteristic.
RE-Rule: this rule sets the edge between two root nodes. For nodes a, b ∈ IA ,
(a, b) : R is considered as a : > 1Rab , a : 6 1Rab , b : > 1Inv(Rab ), b : 6 1Inv(Rab )
with Rab v R and Inv(Rab ) v Inv(R). Therefore, a variable with the value of 1,
σ(v) = 1, for node a that contains Rab represents this edge. The RE-Rule fires and
fills the edge label.
merge-Rule: the merge-Rule merges root nodes. Assume three root nodes a, b, c ∈
IA where b, c are respectively R-successor and S-successor of a. These assertions will
be translated such that we have a : > 1Rab , a : 6 1Rab , a : > 1Sac , a : 6 1Sac with
Rab v R and Sac v S. If there exists a variable v in an arithmetic solution of node a
with Rab , Sac ∈ α(v), it means that c and b need to be merged. The merge-Rule merges
b and c and w.l.o.g replaces every occurrence of b with c and all outgoing/incoming
edges of b become outgoing/incoming edges of c.
ch-Rule: this rule is necessary to ensure the completeness of the algorithm. The
partitions of the atomic decomposition represent all possible combinations of the suc-
cessors of a particular node. The inequation solver has no knowledge about logical
reasons that can force a partition to be empty. Thus, from a semantic branching point of
view we need to distinguish between the two cases v 6 0 and v > 1, where v denotes
the cardinality of a partition.
f il-Rule: the f il-Rule has the lowest priority among the completion rules. This rule
is the only one that generates new nodes, called proxy nodes. For example, if a solution
Ω for a node x includes a variable v with σ(v) = 2, the f il-Rule creates a proxy node y
with cardinality of 2 and sets the edge label and LI (y) as shown in Fig. 2. Since this rule
generates proxy nodes based on an arithmetic solution that satisfies all the inequations,
there is no need to merge the generated proxy nodes later.
The algorithm preserves role hierarchies in its pre-processing phase. If there occurs
a variable v ∈ LE (x), where R ∈ α(v) and S ∈ / α(v) and R v∗ S, then v 6 0.
Therefore, the variables that violate the role hierarchy are set to zero. Due to the space
limitations, we refer for the proof to [12].
4 Practical Reasoning
In this section, we discuss the complexity of our algorithm and evaluate its behavior in
practical reasoning. Let k be the number of all roles occurring in NRs in a TBox after
pre-processing and transforming all QNRs to unqualified ones considering inverse roles.
The search space of the hybrid algorithm depends on the number of variables occurring
in LE labels. Since there are k roles, the number of partitions and their associated
variables is bounded by 2k −1. The ch-Rule creates two branches for each variable: v >
k
1 or v 6 0. Consequently, 22 cases could be examined by the inequation solver and the
worst-case complexity of the algorithm is double exponential. Moreover, the Simplex
method which is used in the hybrid algorithm is NP in the worst case. However, in [11] it
is shown that integer programming is in P in the worst case, if the number of variables
is bounded. The implemented inequation solver (using Simplex method presented in
[1]) minimizes the sum of all variables occurring in the inequations. In addition, we use
several optimization techniques and heuristics that can eliminate branches in the search
space, therefore, avoiding unnecessary invocations of the ch-Rule. These techniques
dramatically improve the average complexity of the hybrid algorithm over the worst
k
case of 22 .
4.1 Optimization Techniques
In most cases, in order to utilize these theoretical algorithms in practice, optimization
techniques are required. Due to the complexity of the algorithm, achieving a good per-
formance may seem infeasible. However, optimization techniques can dramatically de-
crease the size of the search space by pruning many branches. For instance, a stan-
dard technique such as axiom absorption [9] often improves reasoning by reducing the
number disjunctions. Here we explain some of the optimization techniques used in our
hybrid algorithm.
Variable initialization: the inequation solver starts with the default v 6 0 for all
variables and later sets some to v > 1 to satisfy the inequations according to at-least
k
restrictions. Since the ch-Rule is invoked 22 times in the worst case to check variables
for v 6 0 or v > 1, default zero setting of variables prevents unnecessary invocations of
the ch-Rule. Moreover, the boundary value of some of the variables can be determined
from the beginning according to the occurrence of the numbers in at-most or/and at-
least restrictions. For example, if a variable occurs in an at-least restriction but not in an
at-most restriction, then it does not have any arithmetic restriction and is called a don’t
care variable [5]. In addition, the resetIBE -Rule specifically determines the value of
a single variable and sets some of the rest to zero. Similarly, the IBE-Rule sets the
value of some variables to zero and enforces some of the others to be the potential
choices for the answer, therefore, reducing the solution space. Moreover, in order to
avoid unnecessary applications of the resetIBE -Rule additional heuristics are applied.
For a node x, if a role occurs in an at-least restriction but not in any at-most restriction
Algebraic Reasoning for SHIQ 9
106 Hermit
milliseconds)
milliseconds)
(in milliseconds)
(in milliseconds)
106 at-least
Pellet
at-most
FaCT++
Hybrid 104
103
10
Runtime (in
Runtime (in
102
Runtime
Runtime
100 2 3 4 5 6 7 8 9 10
2 2 2 2 2 2 2 2 2 1 3 5 7 9 11 13
Value of k = 2i , 2 i 10 Number of QNRs
Fig. 3. Runtimes for satisfiable concept Fig. 4. Runtimes for concept Test 22 (using a
y-axis)
log scale for the y-axis).
Test 11 (log-log
(log-log scale;
scale; timeout
timeout of 1066 msecs).
of 10 msecs)
and it is not a sub-role of any role R in a concept of the form 8(R ∀(R \ S).C 2 ∈ L(x), then
it cannot be in ↵(v)
α(v) where v represents a back edge for node x.
Dependency-directed backtracking:
backtracking:we weuse
usebacktracking
backtrackingtechniques to findofsources
to find sources logi-
of
callogical
clashesclashes
and thenand then consider
consider the causetheofcause of in
a clash a setting
clash inthesetting the boundaries
boundaries of variablesof
variables in new solutions.
in new solutions. This
This results results in
in pruning pruningwhich
branches branches
would which
lead would lead to
to the same the
clash.
same clash.occurs
If a clash If a clash occurs
in node in nodewas
x, which which was
x, created due created due to va with
to a variable variable
σ(v)v with
= k
and k and
(v) k= ∈ 1, vthen
N, kk 2≥N,1,k then v must
must be set
be set to to zero.
zero. Thisisiscalled
This called simple
simple backtrack-
ing. The previous technique can be improved: if a logical clash is encountered due to
{A, ¬A} 2 ∈ L(x), then the source for propagation of these two concepts to L(x) could
be the roles occurring in 8∀ or 8∀\\ constructs. In this case, the variables which contain
all these roles are set to zero. This is called complex backtracking. These techniques
eliminate many branches in the search space and consequently improving the average
complexity of the algorithm.
4.2 A First Evaluation Using Synthetic Benchmarks
In order to evaluate our hybrid algorithm, a prototype reasoner has been implemented
in Java using the Web Ontology Language API. The reasoner decides satisfiability of
ALCHIQ concepts.
We show the performance of the hybrid reasoner by a set of three benchmarks.
Fig. 3 demonstrates the performance of different DL reasoners for testing the satisfia-
bility of the concept Test 11 defined as C u > 2kRu8R.(>
2kRu∀R.(> kR −.Cu 6 kR −.C), where
ii
k = 2 ,2 ≤i ≤ 10. Fig. 3 compares the reasoning time of our hybrid reasoner with
Pellet, FaCT++, and Hermit.11 All reasoners determine the satisfiability of the concept
in less than ⇠∼ 100 ms before reaching k = 244. While our hybrid reasoner maintains its
reasoning time (constantly under 100 ms), Pellet, Hermit, and FaCT++ start exhibiting
exponential growth in the reasoning time for values higher than k = 244. For exam-
ple, for k = 299 Pellet’s reasoning time is more than 18 minutes and for k = 210 10
it
did not finish within the time limit of 1000 seconds. This example demonstrates the
independent behavior of our hybrid calculus in the presence of higher values in QNRs
interacting with inverse roles.
11
We used an AMD 3.4GHz quad core CPU with 16 GB of RAM.
10
10 RoostaPour
Roosta Pour&&Haarslev
Haarslev
Hermit
Hermit Pellet
Pellet FaCT++
FaCT++ Hybrid-S
Hybrid-S Hybrid-C
Hybrid-C
66 66
10
10 10
10
milliseconds)
milliseconds)
(in milliseconds)
(in milliseconds)
1044
10 1044
10
Runtime (in
Runtime (in
1022
10 1022
10
Runtime
Runtime
1000
10 1000
10
200 400
200 400 600
600 800
800 1,000
1,000 200 400
200 400 600
600 800
800 1,000
1,000
Valueofofkkininsteps
Value stepsofof100
100 Valueofofkkininsteps
Value stepsofof100
100
(a) Unsatisfiable
(a)Unsatisfiable
(a) version
Unsatisfiableversion of
versionof Test
ofTest
Test333 (b)
(b)Satisfiable
(b) Satisfiableversion
Satisfiable versionof
version ofofTest
Test333
Test
Fig. 5.
Fig.5.
Fig. Linear
5.Linear increase
Linearincrease of (using
(usingaaalog
ofkkk(using
increaseof log scale
logscale for
scalefor the
forthe y-axis)
they-axis).
y-axis).
The second
Thesecond
The secondtest test defines
testdefines concept
definesconcept
conceptTest Test
Test222as as
as> > >1S.A
1S.A
1S.Au uu8S.8S.>
∀S. >>1R.B
1R.B
1R.Bu uu8S.8R.8R
∀S.∀R.∀R
8S.8R.8R .P
−
.P
.P
with P defined
withPP defined
with definedasas{uas {u ./
{u././1M 1M1Mii.C.C | 1
i .Ciii| |11≤ i ≤
iik}. k}. Fig.
k}.Fig. 4 shows
Fig.44shows
showsthe the effect
theeffect of increasing
effectofofincreasing
increasingthe the
the
number
numberof
number of at-least
ofat-least
at-leastand and at-most
andat-most restrictions
at-mostrestrictions
restrictionsin in reasoning
inreasoning
reasoningfor for Test222...In
Test
forTest In
Inaaamodel
model
modelfor for the
forthethe
concept
conceptTest
concept Test , the
Test222, ,the concept
theconcept expression
conceptexpression P is
expressionPP isispropagated propagated
propagatedback back
backand and
andwill will
willbe be added
beadded to
addedtotothe the
the
label
labelof
label of
ofaaanode
node
nodewhichwhich already
whichalreadyalreadyhas has
has> > > 1R.B,
1R.B, therefore,
therefore,we
1R.B,therefore, wewehavehave
have(k (k(k+ ++1) 1) QNRs.
QNRs.Since
1)QNRs. Since
Since
for each
foreach
for node
eachnode which
nodewhich whichhas has
hasaaaparent,
parent,
parent,an an IBE
anIBE
IBEwillwill
willbe be considered
beconsidered
consideredas as
asaaaset
set
setofof two
oftwo inequations
twoinequations
inequations
in the
ininthe L
theLLE of
EE of the
ofthe node.
thenode.node.As As shown
Asshown
shownininFig.in Fig. 4, increasing
Fig.4,4,increasing
increasingthe the number
thenumber
numberofofQNRsof QNRs decreases
QNRsdecreases
decreases
the performance
theperformance
the performanceofofthe of the hybrid
thehybrid reasoner.
hybridreasoner.
reasoner.This This is
Thisisisdue due to
duetotothethe fact
thefact that
factthat a
thataalargelarge number
largenumber
numberof of
of
roles in the
rolesininthe
roles QNRs
theQNRsQNRsincreasesincreases
increasesthe the number
thenumber of variables
numberofofvariablesvariablesand and
andthe the size
thesize of
sizeofofthe the search
thesearch space.
searchspace.space.
Comparing
Comparingthe
Comparing the
thetwotwo diagrams
twodiagrams
diagramsin in Fig.
inFig.Fig.4a4a
4aandand
and4b 4b shows
4bshows
showsthat that
thatby by increasing
byincreasing
increasingthe the number
thenumber
number
of at-most
ofofat-most
at-mostQNRs QNRs
QNRsthe the reasoning
thereasoning
reasoningtime time
timeforfor the
forthe arithmetic
thearithmetic reasoner
arithmeticreasoner increases
reasonerincreasesincreasesfaster faster than
fasterthanthan
for at-least
forat-least
for restrictions.
at-leastrestrictions.
restrictions.The The reason
Thereason
reasonisistheis the heuristic
theheuristic
heuristicthat that
thatwewe explained
weexplained in
explainedininSection Section
Section4.1. 4.1. By
4.1.By By
means of
meansofofthis
means this heuristic,
thisheuristic, if
heuristic,ififaarole a role occurs
roleoccurs in
occursininan an at-least
anat-least restriction
at-leastrestriction
restrictionand and
andnot not in
notininanyany at-most
anyat-most
at-most
restriction
restrictionand
restriction and satisfies
andsatisfies
satisfiesthe the pre-conditions
thepre-conditions
pre-conditionsthat that
thatare are mentioned
arementioned
mentionedin in Section
inSection
Section4.1, 4.1, then
4.1,thenthenthethe
the
potential variables
potentialvariables
potential variablesfor for IBE
forIBE which
IBEwhichwhichcontaincontain
containthisthis role
thisrole are
roleare set
areset to zero.
settotozero. Therefore,
zero.Therefore,
Therefore,the the number
thenumber
number
of
of variables
ofvariables
variablesin in the
inthe search
thesearch
searchspacespace
spaceis isisdecreased.
decreased.
decreased.
For the
Forthe
For third
thethird benchmark
thirdbenchmark
benchmarkwe we consider
weconsider
considerthe the concept
theconcept
conceptTest Test defined
definedas
Test333defined as
as>> >8S.Au6
8S.Au6
8S.Au69S.A 9S.A
9S.A
u∀S.(>
u8S.(>kR.C
u8S.(> kR.C
kR.C u uu6 6 66T.D
6T.D
6T.Du uu> > >5T.D)
5T.D)
5T.D)u uu8S.8R.(>
∀S.∀R.(>
8S.8R.(>2T.D 2T.D
2T.Du uu6 6 63T.D)
3T.D)
3T.D)u uu8S.8R.8T.
∀S.∀R.∀T.
8S.8R.8T.
∀T
8T
−
8T .8R.∀R −
.8R .P .P with
.P withwith {R {R
{R v vvM M M}}} 2 ∈2 R R and
Randandkkk 2 ∈2 {100,
{100,
{100,.........,,,1000}.
1000}.
1000}. Fig. Fig.
Fig. 5a 5a displays
5a displays
displays the the
the
runtimes
runtimesfor
runtimes for Test333,,,where
Test
forTest where
whereP PP isisisdefined
defined
definedas as
as6 66(k (k(k− 2)M.(C
2)M.(C
2)M.(Ct ttD).
D).
D).In In this
Inthis example
thisexample
exampleP PP isisis
propagated
propagatedback
propagated back
backand and causes
andcauses
causesthe the unsatisfiability
theunsatisfiability
unsatisfiabilityof of Test333...Fig.
Test
ofTest Fig.
Fig.5b 5b shows
5bshows
showsthe the runtimes
theruntimes
runtimesfor for
for
Test where
whereP
Test333where
Test PPisisisdefined
defined
definedas as
as666(k (k +1)M.(C
(k+1)M.(C
+1)M.(CtD). tD).
tD).In In this
Inthis example
thisexample
exampleP PPis isisalso
also propagated
alsopropagated
propagated
back
backbut
back but does
butdoes
doesnot not result
notresult
resultin in the
inthe unsatisfiability
theunsatisfiability
unsatisfiabilityof of Test333...As
Test
ofTest As expected
Asexpected
expectedthe the hybrid
thehybrid reasoner
hybridreasoner
reasoner
remains stable
remainsstable
remains stablewhilewhile
whilethe the execution
theexecution
executiontimes times
timesof of the
ofthe other
theother reasoners
otherreasoners
reasonersincrease increase according
increaseaccording
accordingto toto
the values
thevalues
the occurring
valuesoccurring
occurringin in the
inthe QNRs.
theQNRs.
QNRs.As As shown
Asshown
shownin in Fig.
inFig.
Fig.5a 5a
5aandand
and5b,5b, Hermit’s
5b,Hermit’s behavior
Hermit’sbehavior behavioris isis
the worst
theworst
the among
worstamongamongall all the
allthe reasoners.
thereasoners.
reasoners.Hermit Hermit
Hermitand and Pellet
andPellet show
Pelletshowshowaaarapid rapid exponential
rapidexponential
exponentialgrowth growth
growth
in
in their
intheir reasoning
theirreasoning
reasoningtimes times
timesas asasaaafunction
function
functionof of
ofk.k. For
k.For Forkkk > > 400, Hermit
400,Hermit
>400, Hermitdid did
didnot not finish
notfinish within
finishwithin
within
the time
thetime
the limit
timelimit
limitof of 1000
of1000 seconds.
1000seconds.
seconds.FaCT++ FaCT++
FaCT++solves solves
solvesthe the problem
theproblem
problemin in
inaaamore
more reasonable
morereasonable
reasonabletime, time,
time,
however,
however,itititdemonstrates
however, demonstrates
demonstratesits its dependency
itsdependency
dependencyon on
onthethe value
thevalue
valueof of
ofkkkas as its
asits runtime
itsruntime increases.
runtimeincreases.
increases.In In
In
addition,
addition,Fig.
addition, Fig. 5
Fig.55showsshows
showsthe the behavior
thebehavior
behaviorofofour of our hybrid
ourhybrid algorithm
hybridalgorithm
algorithmusing using
usingsimplesimple (Hybrid-S)
simple(Hybrid-S)
(Hybrid-S)
and complex (Hybrid-C) dependency-directed backtracking. The complex backtrack-
ing outperforms simple backtracking since it prunes more branches that would lead to
the same sort of clash. In addition to improving the performance of the reasoner the
optimization techniques used in hybrid reasoner can make its performance more stable.
5 Conclusion and Future Work
The hybrid calculus presented in this paper decides SHIQ ABox satisfiability. The
implemented prototype demonstrates the improvement on reasoning time for selected
benchmarks featuring QNRs and inverse roles. Utilizing algebraic reasoning and ap-
plying optimization techniques, the hybrid calculus would be a good solution in case
of large numbers occurring in QNRs. In [2] a hybrid algorithm for SHOQ using alge-
braic reasoning has been proposed and extensively analyzed in an empirical evaluation.
Due to the nature of nominals, [2] needs to use a global partitioning in contrast to the
local partition used in our approach. Several novel techniques to optimize reasoning for
SHOQ have been designed and evaluated in [2]. Some of these techniques are not ex-
clusively dedicated to nominals and could be applied to our hybrid calculus for SHIQ
too. For instance, the exponential number of partitions was addressed using a so-called
lazy partitioning technique which only generates partitions and their associated vari-
ables on demand. We are currently developing a new hybrid prototype for SHIQ that
integrates suitable optimizations techniques from [2]. We are planning to combine our
work on both SHIQ and SHOQ in order to design a hybrid algebraic calculus for
SHOIQ.
References
1. Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. The MIT
Press, 2nd edn. (Sep 2001)
2. Faddoul, J.: Reasoning Algebraically with Description Logics. Ph.D. thesis, Concordia Uni-
versity (September 2011)
3. Faddoul, J., Farsinia, N., Haarslev, V., Möller, R.: A hybrid tableau algorithm for ALCQ. In:
Proceedings of ECAI 2008, Greece. pp. 725–726 (2008)
4. Faddoul, J., Haarslev, V.: Algebraic tableau reasoning for the description logic SHOQ. Jour-
nal of Applied Logic 8(4), 334–355 (December 2010)
5. Farsiniamarj, N., Haarslev, V.: Practical reasoning with qualified number restrictions: A hy-
brid Abox calculus for the description logic SHQ. AI Commun. 23, 205–240 (2010)
6. Haarslev, V., Möller, R.: Optimizing reasoning in description logics with qualified number
restriction. In: Proc. of DL 2001, USA. pp. 142–151 (Aug 2001)
7. Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierar-
chies. Journal of Logic and Computation 9(3), 385–410 (1999)
8. Horrocks, I., Sattler, U., Tobies, S.: Reasoning with individuals for the description logic
SHIQ. In: Proc. of CADE-17. pp. 482–496. Springer-Verlag, London, UK (2000)
9. Horrocks, I., Tobies, S.: Reasoning with axioms: Theory and practice. In: In Proc. of KR
2000. pp. 285–296 (2000)
10. Ohlbach, H.J., Koehler, J.: Modal logics, description logics and arithmetic reasoning. Artif.
Intell. 109, 1–31 (1999)
11. Papadimitriou, C.H.: On the complexity of integer programming. J. ACM 28, 765–768
(1981)
12. Roosta Pour, L.: A Hybrid ABox calculus using algebraic reasoning for the description logic
SHIQ. Master’s thesis, Concordia University (January 2012)