=Paper=
{{Paper
|id=Vol-1635/paper-10
|storemode=property
|title=A Saturation-based Algebraic Reasoner for ELQ
|pdfUrl=https://ceur-ws.org/Vol-1635/paper-10.pdf
|volume=Vol-1635
|authors=Jelena Vlasenko,Maryam Daryalal,Volker Haarslev,Brigitte Jaumard
|dblpUrl=https://dblp.org/rec/conf/cade/VlasenkoDHJ16
}}
==A Saturation-based Algebraic Reasoner for ELQ==
https://ceur-ws.org/Vol-1635/paper-10.pdf
A Saturation-based Algebraic Reasoner for ELQ
Jelena Vlasenko, Maryam Daryalal, Volker Haarslev, and Brigitte Jaumard
Concordia University, Montreal, Quebec, Canada
Abstract
We present a reasoning architecture for deciding subsumption for the
description logic ELQ. Our architecture combines saturation rules with
algebraic reasoning based on Integer Linear Programming (ILP). De-
ciding the so-called numerical satisfiability of a set of qualified cardi-
nality restrictions is reduced to constructing a corresponding system
of linear inequalities and applying ILP methods in order to determine
whether this system is feasible. Our preliminary experiments indicate
that this calculus offers a better scalability for qualified cardinality re-
strictions than approaches combining both tableaux and ILP as well as
traditional (hyper)tableau methods.
1 Introduction and Motivation
We present a reasoning architecture for the description logic (DL) ELQ that is inspired by saturation-based
algorithms for EL [BBL05] but incorporates a new algebraic approach to decide subsumption for ELQ. ELQ
is as expressive as ALCQ because every ALCQ Tbox T can be rewritten to an ELQ Tbox T 0 such that T 0 is
a conservative extension of T . This is possible since ELQ allows one to write axioms denoting disjunction and
negation via QCRs (see Section 3 for an example).
The performance of the original ALCQ tableau algorithm [HB91] that is implemented by most DL reasoners
covering QCRs is not optimal. To perform a concept satisfiability test, this tableau algorithm creates role
successors to satisfy at-least restrictions, e.g. ≥ 20 R.C. Given at-most restrictions, e.g., ≤ 10 R.D, ≤ 10 R.E,
the algorithm resolves each R-successor as either D or ¬D, and E or ¬E. If an at-most restriction for R is
violated (≤ 10 R.D), the algorithm nondeterministically merges two R-successors that are instances of D. This
uninformed process is highly inefficient, especially when the algorithm has to deal with larger cardinalities and/or
large sets of related QCRs. In our previous work (originally inspired by [OK99]) we have shown that algebraic
tableau can improve reasoning on QCRs dramatically for DLs such as SHQ [FH10c], SHIQ [RH12], and SHOQ
[FH10a, FH10b]. The basic idea in these calculi is to transform a set of QCRs into a system of linear inequalities
to be solved by Integer Linear Programming (ILP). If ILP finds a solution to the system of inequalities, i.e.,
the system is feasible, then the corresponding set of QCRs is satisfiable provided completion rules encounter no
logical clashes for the returned numerical solution.
Although the prototypes implementing the above-mentioned approaches on algebraic tableaux [FH10c, RH12,
FH10b] could demonstrate runtime improvements of several orders of magnitude for reasoning about QCRs (and
nominals) we identified the following disadvantageous characteristics: (i) Given n QCRs (and nominals) the
naive encoding of the corresponding system of inequalities requires n rows and 2m columns, where m is the
cardinality of the set P of all the role names and concepts occurring in the n given QCRs. Let us illustrate
this with a small example: ≥ 2R.C u ≥ 2R.D u ≤ 2R.E. In this case, P = {R, C, D, E}, n = 3, m = 4. In
Copyright c by the paper’s authors. Copying permitted for private and academic purposes.
In: P. Fontaine, S. Schulz, J. Urban (eds.): Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning
(PAAR 2016), Coimbra, Portugal, 02-07-2016, published at http://ceur-ws.org
110
P P P P
order to represent the QCRs as inequalities we create xCi ≥ 2, xDj ≥ 2, xDk ≥ 2, and xEl ≤ 2. For
instance, the variables xCi represent the cardinalities of all elements in the power set of P that contain C, R.
The same holds for the other variables respectively. As an additional constraint we specify that all variables
must be greater or equal to zero. Our objective function minimizes the sum of all variables. Intuitively speaking,
the above-mentioned concept conjunction is feasible and in this trivial case also satisfiable if the given system of
inequalities has an integer solution. It is easy to see that the size of such an inequality system is exponential to
m. Furthermore, in order to ensure completeness, we required a so-called choose rule that implements a semantic
split that nondeterministically adds for each variable x either the inequality x ≤ 0 or x ≥ 1. Unfortunately, this
m
uninformed choose rule could fire 22 times in the worst case and cause a severe performance degradation.
(ii) The employed ILP algorithms were best-case exponential in the number of occurring QCRs due to the
explicit representation of 2m variables. In [FH10a, FH10b] we developed an optimization technique called lazy
partitioning that tries to delay the creation of ILP variables but it cannot avoid the creation of 2m variables
in case m QCRs are part of a concept model. Our experiments in [FH10a, FH10b, FH10c] indicated that
quite a few ILP solutions can cause clashes due to lack of knowledge about known subsumptions, disjointness,
and unsatisfiability of concept conjunctions. This knowledge can help reducing the number of variables and
eliminating ILP solutions that would fail logically. For instance, an ILP solution for the example presented in
the previous paragraph might require the creation of an R-successor as an instance of C u D u ¬E. However, if
C and D are disjoint this ILP solution will cause a clash (and fail logically).
Characteristic (i) can be avoided by eliminating the choose rule for variables. This does not sacrifice complete-
ness because the algorithms implementing our ILP component are complete (and certainly sound) for deciding
(in)feasibility. In case a system is feasible (or numerically satisfiable), dedicated saturation rules determine
whether the returned solutions are logically satisfiable. In case of logical unsatisfiability a corresponding unsat-
isfiable concept conjunction is added to the input of the ILP component and therefore monotonically constrains
the remaining feasibility space. Consequently, previously computed solutions that result in unsatisfiability are
eliminated. For instance, the example above would be deemed as infeasible once the ILP component learns that
C and D are subsumed by E and that C and D are disjoint.
The avoidance of characteristic (ii) is motivated by the observation that only a small number of the 2m
variables will have non-zero values in the optimal solution of the linear relaxation, i.e., no more variables than
the number of constraints following the characteristics of the optimal solution of a linear program, see, e.g.,
[Chv83]. As a consequence, only a limited number of variables have a nonzero value in the integer optimal
solution. In addition, linear programming techniques such as column generation [DW60, GG61] can operate
with as few variables as the set of so-called basic variables in linear programming techniques at each iteration,
i.e., nonbasic variables can be eliminated and are not required for the guarantee of reaching the conclusion that a
system of linear inequalities is infeasible, or for reaching an optimal LP solution. Although the required number
of iterations varies from one case to another, it is usually extremely limited in practice, in the order of few times
the number of constraints. The efficiency of the branch-and-price approach, which is required in order to derive
an ILP solution, see, e.g., [BJN+ 98, Van11, LD05], depends on the quality of the integrality gap (i.e., how far
the optimal linear programming solution is from the optimal ILP solution in case the system of inequalities
is feasible, and on the level of infeasibility otherwise). Several studies have been devoted to improving the
convergence of column generation algorithms, especially when degeneracy occurs (see, e.g., [DGL14]) or when
convergence is too slow (see, e.g., [ADF09]), and to accelerating the convergence of branch-and-price algorithms
[DDS11]. Furthermore, our ILP component considers known subsumptions, disjointness, and unsatisfiability of
concept conjunctions and uses a different encoding of inequalities that already incorporates the semantics of
universal restrictions. We delegate the generation of inequalities completely to the ILP component.
To summarize, the novel features of our architecture are (i) saturation rules that do not backtrack to decide
subsumption (and disjointness); (ii) feasibility of QCRs is decided by ILP (in contrast to [BMC+ 16]); (iii)
our revised encoding of inequalities and the aggregation of information about subsumption, disjointness, and
unsatisfiability of concept conjunctions allows a more informed mapping of QCR satisfiability to feasibility and
reduces the number of returned solutions that fail logically; (iv) the best-case time complexity of our ILP
feasibility test is polynomial to the number of inequalities [Meg87]. In the following sections we present our
saturation rules, introduce our ILP approach, sketch soundness, completeness, and termination, present our
preliminary evaluation results, and conclude with a summary and future work.
111
2 A Calculus for ELQ
The DL ELQ allows the concept-forming constructors u (conjunction), ≤ (at-most restriction), and ≥ (at-least
restriction). The semantics of ELQ concepts and roles is defined by an interpretation I = (∆I , ·I ) that maps
a concept A ∈ NC (NC is a set of concept names) to AI ⊆ ∆I and a role R ∈ NR (NR is a set of roles) to
RI ⊆ ∆I × ∆I . We assume the predefined concepts > and ⊥ with >I = ∆I and ⊥I = ∅. ELQ concepts are
inductively defined from the sets NC and NR using the constructors as follows (n, m ∈ N, n ≥ 1, k · k denotes set
cardinality, F R,C (x) = {y ∈ C I | (x, y) ∈ RI }): (i) (C u D)I = C I ∩ DI ; (ii) (≥ n R.C)I = {x | kF C,R (x)k ≥ n};
(iii) (≤ m R.C)I = {x | kF C,R (x)k ≤ m}. The latter two constructors are called QCRs. A concept C is satisfiable
if there exists an I such that C I 6= ∅.
An ELQ Tbox T is defined as a finite set of axioms of the form C v D and such an axiom is satisfied by I if
C I ⊆ DI . We call I a model of T if it satisfies all axioms in T . We use CAT to denote the set that contains >
Q
and all concept names used in T , C¬A A
T = {¬A | A ∈ CT \ {>}}, CT to denote the set that contains all QCRs (and
A ¬A Q
their negation) used in T , and define CT = CT ∪ CT ∪ CT . We use RT to denote the set of roles used in T .
A Tbox T is normalized if all axioms are of the form A1 v B, A1 v ./ n R.A2 , ./ n R.A1 v B, A1 u A2 v B,
with B ∈ CAT ∪ {⊥}, A1 , A2 ∈ CAT , and ./ ∈ {≥, ≤}. It is easy to see that this can be done in polynomial time
following the normalizations described in [BBL05, Kaz09, SMH14]. A normalized Tbox is always in negation
normal form because it does not allow the occurrence of negation. Some of our saturation rules make use of
the negation operator ¬˙ which returns the negation normal form for named concepts and QCRs defined as
¬(C)
˙ = ¬C, ¬(¬C)
˙ = C, ¬(≤
˙ m R.C) = ≥ m+1 R.C, and ¬(≥ ˙ n R.C) = ≤ n−1 R.C for m ≥ 0, n ≥ 1.
We adopted the idea of saturation graphs from [BBL05, SGL14]. Our saturation graphs have been extended
to deal with ELQ and delegate numerical reasoning on QCRs to an ILP component.
A saturation graph G = (V, E, L, LP , L¬ P ) is a directed graph where V = VP ∪VA ∪VC such that VP , VA , VC are
pairwise disjoint. VP = {vA | A ∈ CAT } is the set of predefined nodes, VA = {vS | S ⊆ CAT } the set of anonymous
nodes representing role successors, and VC is the set of nodes called QCR clones representing subsumption or
disjointness tests based on QCRs. Each node vS ∈ V uniquely represents either an element (S ∈ L(vS )) of
CAT or a subset (S ⊆ L(vS )) of CAT ∪ C¬A T . We also call S the initial label of vS . Each v ∈ V is labelled with
Q
a set of concepts L ⊆ CT ∪ {⊥} and sets of subsumption tuples LP , L¬ A
P ⊆ {hp, qi | p ⊆ CT , q ⊆ CT }. Each
0 0 0
edge hv, v i ∈ E is labelled with a set L(v, v ) ⊆ RT where v is called an r-successor (R-successor) of v with
r ⊆ L(v, v 0 ) (R ∈ L(v, v 0 )).
Given a normalized Tbox T and a corresponding saturation graph G the label set LP (L¬ P ) contains tuples
specifying subsumption (disjointness) conditions caused by QCRs. A subsumption tuple of the form hp, qi consists
of a set of precondition concepts p ⊆ CAT and a set of QCRs q ⊆ CQ T . Some of the rules that operate on LP
and L¬ P make use of special (negated) membership (∼∈ , is new), subset (⊂ ∪) operators, and a map (ϕ)
∼ ), union (∼
operator. We define is new(q, S) = h{>}, {q}i ∼ ∈
/ S and add to(Q, S) as S ← S ∼ ∪ {h{>}, {Q}i} if Q is a QCR or
S←S∼ ∪ Q if Q is a set of subsumption tuples.
Given sets T, T 0 of subsumption tuples, hp, qi ∼ ∈ T is true if there are p0 , q 0 such that hp0 , q 0 i ∈ T , p ⊆ p0 , and
0 0 0
q⊆q;T ⊂ ∼ T is true if ∀t ∈ T ⇒ t ∼ ∈ T holds. {hp1 , s1 i} ∼ ∪ {hp2 , s2 i} is defined as {hp2 , s1 ∪ s2 i} if p1 ⊆ p2 and
{hp1 , s1 i, hp2 , s2 i} otherwise. The map operator is defined as ϕ(A, T ) = {hp ∪ {A}, qi | hp, qi ∈ T } with A ∈ CAT .
Our saturation rules interface the ILP component via the predicate infeasible(S) which transforms all QCRs
in S to a corresponding system of inequalities and returns true if this system is infeasible. Otherwise it returns
false. If S contains no QCRs it also returns false. A node v is called numerically satisfiable or feasible, if the set
Q ⊆ L(v) of QCRs is feasible. A concept A is called feasible if its node vA is feasible. The number of possible
solutions for a feasible node can be huge1 and quite a few solutions might eventually cause logical unsatisfiability.
In order to ensure termination and logically constrain the number of possible solutions for a node v as much as
possible, the ILP component makes use of concept information derived from a Tbox T and its saturation graph
G. For a node v ∈ VP ∪ VA we define Qv = {C | ./ n R.C ∈ L(v)} ∪ {¬D | ≤ 0 R.D ∈ L(v)} as the set of QCR
qualifications occurring in L(v). The information aboutSconcept unsatisfiability and subsumption, which is used
by the ILP component, is defined by the set unsat S= v∈VP ∪VA unsat v , which contains sets of concepts whose
conjunction is unsatisfiable, and the set subs v = v∈VP ∪VA subs v , which contains sets of tuples representing
entailed subsumption relationships of the form A v B or A1 u A2 v B.
unsat v = {{A} | A ∈ Qv , ⊥ ∈ L(vA )} ∪ {q | q ⊆ Qv , ⊥ ∈ L(vq ), vq ∈ VA } ∪
{{Ai , Aj } | ¬Ai ∈ L(vAj ), {Ai , Aj } ∩ Qv 6= ∅, i, j ∈ 1..2, i 6= j}
1 In [FH10c, Sec. 4.1.1] it was shown that if a node label contains p (q) QCRs of the form ≥ n R .C (≤ m R0 .C 0 ), then 2qN
i i i j j j
cases/solutions can exist with N = pi=1 ni .
P
112
subs v = {h{A1 , A2 }, Bi | {A1 , A2 } ⊆ Qv , C1 u C2 v D ∈ T , Ci ∈ L(vAi ), B ∈ L(vD ), i ∈ 1..2} ∪
{h{A}, Bi | B ∈ L(vA ), A ∈ Qv }
In case a node v is numerically satisfiable, the set σ(v) contains solutions for feasible inequality systems
denoted by the QCRs in L(v). A QCR solution is described by a set of tuples of the form hr, q, ni with r ⊆ RT
and q ⊆ CAT ∪ C¬AT sets of roles and concepts respectively, and n denotes the cardinality of the set of r-successors
that are instances of all concepts contained in q.
A saturation graph G is initialized with representative nodes for all concepts in CAT . For instance, for a concept
A a node vA is created with L(vA ) = {>, A} and LP (vA ) = L¬ P (vA ) = ∅. The saturation rules are applied to an
initialized saturation graph until no rule is applicable anymore. Only the vP4 -Rule and v¬ P4 -Rule with v ∈ VC
can be applied to a node v if ⊥ ∈ L(v).
This algorithm computes the named subsumers for all predefined nodes and, thus, decides satisfiability and
subsumption for all concepts in CAT . A concept A is satisfiable iff ⊥ ∈ / L(vA ), and A is subsumed by B iff
B ∈ L(vA ). The top section of Figure 1 contains five rules. The v-Rule (v¬ -Rule) allows a QCR or named
concept on its right-hand (left-hand) side. The v∗ -Rule ensures that L(v) contains all QCRs and (negated) named
concepts inherited from its subsumers. The vu -Rule is a standard EL rule complemented by its contrapositive
version (v¬ u -Rule). The second section contains two rules that deal with role successors where # denotes the
cardinality of an anonymous node. If hr, q, ni ∈ σ(v) the fil-rule and e-rule ensure that an edge r ⊆ L(v, vq )
exists that connects v to an anonymous successor vq with L(vq ) = q and #vq = n, i.e., vq represents n identical
r-successors of v.
For a node v the ⊥-Rule records clashes by adding ⊥ to L(v). For a node v 0 created by the fil-rule there is
no need to propagate ⊥ to its predecessor v because v 0 represents one of possibly many existing QCR solutions
for v. If all QCR solutions for v fail, the ILP component eventually determines that v is infeasible and thus
unsatisfiable.
The fourth section of Figure 1 contains five rules that create and maintain subsumption tuples. Only three
¬
of these rules (P./ -Rule, P./ -Rule, Pu -Rule) derive tuples from axioms. The other two rules propagate tuples up
¬
(vP -Rule) or down (vP -Rule) the subsumption hierarchy.
The bottom section of Figure S 1 lists rules that discover subsumptions or disjointness due to subsumption
tuples. Q(v, S) is defined as hp,qi∈S {q | p ⊆ L(v)} and contains applicable QCRs selected from the set S of
subsumption tuples. The relation clone ⊆ V × (CAT ∪ CT¬A ) × V keeps track of subsumption or disjointness tests
and their associated QCR clones. For instance, a QCR clone v 0 ∈ VC of vA contains all QCRs contained in
L(vA ) and LP (vB ) (L¬ 0
P (vB )) and represents the test whether A is subsumed by (disjoint to) B. If v becomes
unsatisfiable, then B (¬B) is added to L(vA ). The vP1 -Rule creates necessary QCR clones, the vP2 -Rule (vP3 -
Rule) ensures that Q(vA , LP (vB )) (L(vA ) ∩ CQ 0
T ) is contained in L(v ). The vP4 -Rule adds B to L(vA ) if vA ’s
corresponding clone is unsatisfiable. The other four rules deal with disjointness in an analogous way.
3 Small Tbox Example Illustrating Rule Application
We demonstrate our calculus with a small ALCQ Tbox T which entails C v D1 u ¬D2 (see below). A slightly
different example (C-SAT-exp-ELQ) is also used in our synthetic benchmark (see Section 6) and surprisingly
none of the tested reasoners besides Avalanche and Racer can classify the version with n = 10 within a time
limit of 1000 seconds.
C v ≥ 20 R.> u ≤ 10 R.A u ≤ 10 R.B
C v D1 t D2
D1 v ≤ 10 R.¬A, D2 v ≤ 9 R.¬B
The following steps show our rewriting of T into T 0 , which is a normalized ELQ Tbox that is a conservative
extension of T .
1. We remove the occurrence of t and add the entailment C v D1 t D2 using fresh concepts X3 , X4 and a
fresh role S1 .
C v ≥ 20 R.> u ≤ 10 R.A u ≤o10 R.B
C u ≥ 1 S1 .(X3 u X4 ) v D1 These two axioms entail C v D1 t D2
C u ≥ 2 S1 .> v D2
D1 v ≤ 10 R.¬A
D2 v ≤ 9 R.¬B
2. We normalize the axioms (but allow a conjunction on the right-hand side for sake of brevity) and replace
¬A, ¬B by notA, notB and new axioms using fresh roles S2 , S3 such that ¬notA v A and ¬notB v B are
113
v-Rule if A v φ ∈ T , φ ∈ / L(vA )
then add φ to L(vA )
v¬ -Rule if φ v A ∈ T , ¬A ∈ L(v), ¬φ ˙ ∈ / L(v)
then add ¬φ ˙ to L(v)
v∗ -Rule if A ∈ L(v), τ ∈ L(vA ), τ ∈ / L(v)
then add τ to L(v)
vu -Rule if A1 u A2 v B ∈ T , {A1 , A2 } ⊆ L(v), B ∈ / L(v)
then add B to L(v)
v¬
u -Rule if Ai u Aj v B ∈ T , {¬B, Ai } ⊆ L(v), ¬Aj ∈ / L(v)
then add ¬Aj to L(v)
fil-Rule if hr, q, ni ∈ σ(v), ¬∃ vq ∈ V : q ⊆ L(vq ), #vq ≥ n
then create vq ∈ VA with L(vq ) ← q and #vq ← n
e-Rule if hr, q, ni ∈ σ(v), q ⊆ L(vq ), #vq ≥ n, r * L(v, vq )
then add r to L(v, vq )
⊥-Rule if ⊥ ∈ / L(v) ∧ (infeasible(L(v)) ∨ {A, ¬A} ⊆ L(v))
then add ⊥ to L(v)
P./ -Rule if ./ n R.A v B ∈ T , is new(¬(./ ˙ n R.A), LP (vB ))
then add to(¬(./˙ n R.A), LP (vB ))
¬
P./ -Rule if A v ./ n R.B ∈ T , is new(./ n R.B, L¬ P (vB ))
then add to(./ n R.B, L¬ P (v B ))
P -Rule if B ∈ L(vA ), LP (vA ) 6⊂ ∼ LP (vB )
then add to(LP (vA ), LP (vB ))
P ¬ -Rule if B ∈ L(vA ), L¬ 6⊂ ¬
P (vB ) ∼ LP (vA )
then add to(LP (vB ), L¬
¬
P (vA ))
Pu -Rule if Ai u Aj v B ∈ T , ϕ(Ai , LP (vAj )) 6⊂ ∼ LP (vB )
then add to(ϕ(Ai , LP (vAj )), LP (vB ))
vP1 -Rule if Q(v, LP (vB )) 6= ∅, {B, ¬B} ∩ L(v) = ∅, clone(v, B) = ∅
then create v 0 ∈ VC , L(v 0 ) ← {>}, clone(v, B) ← {v 0 }
vP2 -Rule if v 0 ∈ clone(v, B), {B, ¬B} ∩ L(v) = ∅, Q(v, LP (vB )) * L(v 0 )
then add to(Q(v, LP (vB )), L(v 0 ))
vP3 -Rule if v 0 ∈ clone(v, B), {B, ¬B} ∩ L(v) = ∅, L(v) ∩ CQ 0
T * L(v ) ∩ CT
Q
Q 0
then add to(L(v) ∩ C , L(v ))
vP4 -Rule if {B, ¬B} ∩ L(v) = ∅, v 0 ∈ clone(v, B), ⊥ ∈ L(v 0 )
then add B to L(v)
v¬
P1 -Rule if Q(v, L¬ P (vB )) 6= ∅, {B, ¬B} ∩ L(v) = ∅, clone(v, ¬B) = ∅
then create v 0 ∈ VC , L(v 0 ) ← {>}, clone(v, ¬B) ← {v 0 }
v¬
P2 -Rule if v 0 ∈ clone(v, ¬B), {B, ¬B} ∩ L(v) = ∅, Q(v, L¬ 0
P (vB )) * L(v )
¬ 0
then add to(Q(v, LP (vB )), L(v ))
v¬
P3 -Rule if v 0 ∈ clone(v, ¬B), {B, ¬B} ∩ L(v) = ∅, L(v) ∩ CQ 0
T * L(v ) ∩ CT
Q
then add to(L(v) ∩ CQ , L(v 0 ))
vP4¬ -Rule if {B, ¬B} ∩ L(v) = ∅, v 0 ∈ clone(v, ¬B), ⊥ ∈ L(v 0 )
then add ¬B to L(v)
Figure 1: Saturation rules (φ ∈ CAT ∪ CQ
T , τ ∈ CT ; ./ ∈ {≥, ≤}; i, j ∈ 1..2, i 6= j)
114
entailed. This Tbox T 0 additionally entails C v X5 u ¬X7 .
C v ≥ 20 R.> u ≤ 10 R.A u ≤ 10 R.B
C u X5 v D1
≥ 1 S1 .X6 v X5
X3 u X4 v X6
C u X7 v D2
≥ 2 S1 .> v X7
D1 v ≤ 10 R.notA
D2 v ≤ 9 R.notB
≤ 1 S2 .> v notA
o
These two axioms entail ¬notA v A
≥ 1 S2 .> v A
≤ 1 S3 .> v notB
o
These two axioms entail ¬notB v B
≥ 1 S3 .> v B
3. Known subsumptions or unsatisfiability of concept conjunctions are derived from T 0 .
subs = {h{C, X5 }, D1 i, h{C, X7 }, D2 i, h{X3 , X4 }, X6 i}
unsat = ∅
¬
4. After applying the rules v, P./ , P./ , Pu we get the following node labels (for sake of better readability we
denote vA , where A is a concept name, simply as A when used for the labels L, LP , L¬ P ; anonymous and
clone nodes are denoted as vai and vcj respectively).
L(C) = {>, C, ≥ 1 S1 .X3 , ≥ 1 S1 .X4 , ≥ 20 R.>, ≤ 10 R.A, ≤ 10 R.B}
σ(C) = {h{R}, {¬A, ¬B, ¬notB }, 20i, h{S1 }, {X3 , X4 , X6 }, 1i}
L¬P (C) = {h{>}, {≥ 1 S1 .X3 }i, h{>}, {≥ 1 S1 .X4 }i, h{>}, {≥ 20 R.>}i, h{>}, {≤ 10 R.A}i,
h{>}, {≤ 10 R.B}i}
L(D1 ) = {>, D1 , ≤ 10 R.notA}
L¬P (D1 ) = {h{>}, {≤ 10 R.notA}i}
LP (D1 ) = {h{>, C}, {≤ 0 S1 .X6 }i
L(D2 ) = {>, D2 , ≤ 9 R.notB }
L¬P (D2 ) = {h{>}, {≤ 9 R.notB }i}
LP (D2 ) = {h{>, C}, {≤ 1 S1 .>}i
LP (X5 ) = {h{>}, {≤ 0 S1 .X6 }i}
LP (X7 ) = {h{>}, {≤ 1 S1 .>}i}
LP (notA) = {h{>}, {≥ 2 S2 .>}i}
LP (A) = {h{>}, {≤ 0 S2 .>}i}
LP (notB ) = {h{>}, {≥ 2 S3 .>}i}
LP (B) = {h{>}, {≤ 0 S3 .>}i}
5. After applying the rules v¬ ¬ ¬
P1 , vP2 , vP3 (is C disjoint to D2 ?) and creating the clone vc1
clone(C, ¬D2 ) ← vc1
L(vc1 ) = {>, ≥ 1 S1 .X3 , ≥ 1 S1 .X4 , ≥ 20 R.>, ≤ 10 R.A, ≤ 10 R.B, ≤ 9 R.notB }
6. After applying the fil- and e-rule for vc1 and the rules v¬ , ⊥ for va1
σ(vc1 ) = {h{R}, {¬A, ¬B, ¬notB }, 20i, h{S1 }, {X3 , X4 , X6 }, 1i}
L(vc1 , va1 ) = {R}
L(va1 ) = {>, ¬A, ¬B, ¬notB , ≤ 0 S2 .>, ≤ 0 S3 .>, ≥ 2 S3 .>, ⊥}, #va2 = 20
L(vc1 , va2 ) = {S1 }
L(va2 ) = {>, X3 , X4 , X6 }, #va2 = 1
Based on the unsatisfiability of va1 we add {¬A, ¬B, ¬notB } to unsat.
7. After applying the fil- and e-rule for vc1 again, the rules v¬ , ⊥ for va3
σ(vc1 ) = {h{R}, {¬A, ¬B, notB }, 9i, h{R}, {¬A, B, ¬notB }, 1i, h{R}, {A, ¬B, ¬notB }, 10i,
h{S1 }, {X3 , X4 , X6 }, 1i}
L(vc1 , va3 ) = {R}
L(va3 ) = {>, ¬A, ¬B, notB , ≤ 0 S2 .>, ≤ 0 S3 .>}, #va3 = 9
L(vc1 , va4 ) = {R}
L(va4 ) = {>, ¬A, B, ¬notB , ≤ 0 S2 .>, notA, ≥ 2 S3 .>}, #va4 = 1
115
L(vc1 , va5 ) = {R}
L(va5 ) = {>, A, ¬B, ¬notB , ≤ 0 S3 .>, notB , ⊥}, #va2 = 10
Based on the unsatisfiability of va5 we add {A, ¬B, ¬notB } to unsat. Together with the previous addition
to unsat we learned that {¬B, ¬notB } is unsatisfiable.
8. The ⊥-rule adds ⊥ to L(vc1 ) because infeasible(L(vc1 )) is true due to {¬B, ¬notB } ∈ unsat.
9. The v¬
P4 -rule adds ¬D2 to L(C).
10. The rules v¬ ¬
u and v add ¬X7 and ≤ 1 S1 .> to L(C).
11. After applying the rules vP1 , vP2 , vP3 (is C subsumed by X5 ?) and creating the clone vc2
clone(C, X5 ) ← vc2
L(vc2 ) = {>, ≥ 1 S1 .X3 , ≥ 1 S1 .X4 , ≥ 20 R.>, ≤ 10 R.A, ≤ 10 R.B, ≤ 1 S1 .>, ≤ 0 S1 .X6 }
12. The ⊥-rule adds ⊥ to L(vc2 ) because infeasible(L(vc2 )) is true due to role S1 .
13. The vP4 -rule adds X5 to L(C).
14. The vu -rule adds D1 to L(C).
Other rules are still applicable but for sake of brevity we do not illustrate their application. Furthermore, no
other concept subsumptions are entailed w.r.t. T .
4 ILP Component
We now present the large-scale optimization framework we have designed for solving the system of QCRs in
the DL ELQ. It is based on a decomposition technique, called DantzigWolfe decomposition or more commonly
column generation technique [Las70, Chv83], combined with a branch-and-price technique [BJN+ 98] in order to
either detect that the system is infeasible, or to compute an optimal solution of the system.
Given T , v ∈ V and S containing QCRs, define the qualifying role set of v as SQ = {α(./ nR.C) | ./ nR.C ∈
S} ∪ {C | ./ nR.C ∈ S} ∪ {>, ⊥}, where α defines a mapping between a QCR and its associated (proxy) subrole
of R that is new in T , e.g., α(./ nR.C) = R0 with R0 v R and R0 new in T . The role partitioning PSQ of a
qualifying role set SQ is defined as the power set of SQ (without the empty set). Note that a qualifying concept
can be a member of a partition at least one role. For each partition p ∈ PSQ ,
S only if the partition also containsT
we define pI = fil (v, p) ∩ (∆I \ Y ∈SQ \p fil (v, Y )) where fil (v, p) = e∈p fil (v, e) and fil (v, e) = eI if e is a concept
and fil (v, e) = {y I | (v I , y I ) ∈ eI } if e is a role. The semantics of role partitions in PSQ is defined in such a
way that their interpretations are pairwise disjoint. The absence of a role or concept in a partition implies the
presence of its semantic negation. We now define a mapping ξ from S to a linear inequality system as follows:
- ξ(≥ nR.C) = { q∈PS |R0 ∈q xq ≥ n} with R0 = α(≥ nR.C),
P
Q
- ξ(≤ nR.D) = { q∈PS |R00 ∈q xq ≤ n} ∪ q∈Q {xq ≤ 0}, such that Q = {p ∈ PSQ | D ∈ p ∧ R00 ∈
P S
/ p}, with
Q
R00 = α(≤ nR.D).
S
In order to determine whether ξ(S) = ./nR.C∈S ξ(./ nR.C) is feasible using a highly scalable solution, we
propose a column generation ILP formulation for expressing ξ(S) as a mathematical ILP model, which will be
solved using a branch-and-price algorithm [BJN+ 98].
Given T , v ∈ V , S, SQ and PSQ , the ILP model associated with the feasibility problem of ξ(S) can be written
as follows:
X
min costp xp (1)
p∈PSQ
X 0 ≥role
subject to: aR
p xp ≥ δ R 0 R0 ∈ SQ (2)
p∈PSQ
X 0 ≤role
aR
p xp ≤ δ̄R0 R0 ∈ SQ (3)
p∈PSQ
xp ∈ Z+ p ∈ PSQ , (4)
116
≥role ≤role ≥role ≤role
where SQ = {α(≥ nR.C) | ≥ nR.C ∈ S}, SQ = {α(≤ nR.C) | ≤ nR.C ∈ S}, SQ role
= SQ ∪ SQ ,
δ R0 (δ̄R0 ) is the cardinality of an at-least (at-most) restriction on a subrole R0 ∈ SQ role
, and xp represents a
partition of the set PSQ . costp is defined as the number of concepts in partition p.
When the set of inequalities has a non empty solution set, we are interested in partitions that only contain the
entailed concepts, i.e., the minimum number of concepts that are needed to satisfy all the axioms. Consequently,
in the objective, costp ensures that output partitions only contain the entailed concepts, i.e., the minimum
number of concepts that are needed to satisfy all the axioms.
In order to design a scalable solution of (1)-(4), which has an exponential number of variables, we consider
a solution scheme that makes use of an implicit representation of the constraint matrix. This corresponds to
using a branch-and-price method, a generalization of a branch-and-bound method [NW88] in which the linear
relaxation of (1)-(4) is solved with a column generation algorithm ([Las70], [Chv83]). The linear relaxation is
defined by (1)-(3) and constraint (40 ), which is written as follows:
x p ∈ R+ p ∈ PSQ . (40 )
Next step is to use an implicit representation of all the variables of (1)-(40 ). Therefore, instead of defining the
variables for p ∈ PSQ , we do it for p ∈ PS0 Q ⊆ PSQ , leading to the so-called restricted ILP or restricted master
problem in the mathematical programming literature, in which constraints (40 ) are replaced by constraints
x p ∈ R+ p ∈ PS0 Q , (400 )
with PS0 Q = ∅ at the outset. We next have an iteration solution process in which, at each iteration, the column
generation algorithm tries to generate an improving partition p, i.e., a partition such that, if added to the current
PS0 Q , improves the objective of formulation (1)-(400 ). The partition generator (PG), also called pricing problem
in the mathematical programming literature, is a mathematical ILP model with two sets of decision variables:
0
aR = 1 if role R0 is in the generated partition, 0 otherwise ; bC = 1 if concept C ∈ SQ concept
is in the generated
concept
partition, 0 otherwise, where SQ containing all the concepts of SQ and no subrole. The (PG) model can be
stated as: X X 0 0 X 0 0
(PG) min bC − aR π̂ R − aR ω̂ R (5)
concept
C∈SQ ≥role ≤role
R0 ∈SQ R0 ∈SQ
0 ≥role
subject to: aR ≤ bC R0 ∈ SQ , C = R0 .qualif ier (6)
0 ≤role
bC ≤ aR R0 ∈ SQ , C = R0 .qualif ier (7)
concept
bC ≤ b> C ∈ SQ (8)
b⊥ = 0 (9)
0
bC , aR ∈ {0, 1} R0 ∈ SQ
role concept
, C ∈ SQ role
= SQ \ SQ , (10)
0 0
where π̂ R and ω̂ R are the optimal values of the dual variables of problem (1)-(400 ) (see [Chv83] if not familiar
with linear programming concepts). The objective function (5) is the so-called reduced cost of a partition (or
column, see again [Chv83] for more details on the column generation method). Constraints (6)-(10) implement
the semantics of ξ(S).
(PG) returns a valid partition of PSQ , assuming no other information is provided. In its feasibility space, it
contains a 1-to-1 mapping between the said partitions and algebraic inequalities. If other informations such as:
(i) subsumption (T |= A v B), (ii) binary subsumption (A u B v C) and (iii) disjointness (T |= A1 u · · · u An v
⊥, n ≥ 1) are provided, the cardinality of some partitions p ∈ PSQ might need to be 0. Depending on the
information received, the semantics can be implemented by (in)equalities, using a 1-to-1 mapping presented
below.
- For every T |= A v B, set SQ concept
= SQconcept
∪ {A, B} and add bA ≤ bB to (PG), in order to guarantee
that if a generated partition contains a certain concept, it does contain all its subsumers.
- For every T |= A u B v C, update SQ concept concept
= SQ ∪ {A, B, C} and add bA + bB − 1 ≤ bC to (PG).
Then, if (PG) generates a partition containing A and B, it must contain C as well.
- For every disjointness relation T |= A1 u · · · u An v ⊥, n ≥ 1, set SQ
concept concept
= SQ ∪ {A1 , . . . , An } and
Pn
add i=1 bAi − n + 1 ≤ b⊥ to (PG). This inequality ensures that if all the concepts Ai , i = 1, . . . , n are
present in a partition; this partition cannot be generated since otherwise it would contain ⊥ as well.
117
Figure 2: Overview of ILP solution process
- If there is some concept C with ¬C ∈ SQ
concept
, the relationship of C and ¬C can be modelled with equality
bC + b¬C = 1. This implies that every generated partition contains exactly one of C and ¬C.
Every partition generated by (PG), which possibly contains some of the above inequalities or equalities,
satisfies all the input axioms except the QCRs, which are taken care of in (1)-(400 ). The column generation
method is an iterative process in which (1)-(400 ) and (PG) are alternatively solved until (PG) cannot provide any
new improving partitions, i.e., when the optimal value of the objective of (PG) is positive. This corresponds to
one of the optimality conditions when solving a linear program, see, e.g., [Chv83] for more details.
In the branch-and-price algorithm, an implicit enumeration scheme with a breadth first search (BFS) explo-
ration strategy, branching is done upon a subrole R0∗ selected as follows:
X 0
R0∗ = arg 0max aR
p × max {x̂ p − bx̂ p c, dx̂ p e − x̂ p } , (11)
R ∈SQrole
0
p∈P
0∗ 0∗
leading to two branches, one with aR = 0 and the other one with aR = 1. This branching scheme is clearly
exhaustive and valid (see [Van11] and [NW88]). The branch-and-price algorithm terminates when either an
integer feasible solution for (1)-(4) is found, or an infeasibility is detected, i.e., either the linear programming
relaxation (1)-(400 ) has no solution (in most of the infeasibility cases) or the branch-and-price algorithm fails
to find a feasible integer solution, see [NW99]. A flowchart is provided in Figure 2 to summarize the solution
process.
Soundness and Completeness
The mapping presented in the previous paragraphs is a one-to-one mapping between the axioms and the algebraic
inequalities. Thus, the feasibility space defined by (2)-(4) represents all the instances that satisfy all axioms.
Following the decomposition ILP model that is proposed, constraints related to satisfying QCRs are addressed
in (2)-(4), while all other axioms are embedded in (PG). The branch-and-price algorithm, if (1)-(4) is feasible,
returns one set of valid partitions, and the selection of them is made by the objective (1).
118
The result of the proposed solution process is sound. Indeed, every model produced by the large-scale opti-
mization framework, i.e., ILP model (1)-(4) and branch-and-price algorithm, satisfies all the axioms that are fed
to the ILP component. It is also complete, because the feasibility spaces of the (1)-(400 ) and (PG) consider all
the possible models through the one-to-one mapping that leads to ILP model (1)-(4). In addition, the branching
rule in the branch-and-price algorithm considers a partitioning of the overall solution space, therefore no solution
is left out.
5 Soundness and Completeness
Due to lack of space we can only sketch the soundness and completeness proofs for our saturation rules. Given
the presentation in the previous section we know that the algorithms implementing the ILP component are
sound and complete and terminate in finite time for deciding whether a set of QCRs is feasible, i.e., numerically
satisfiable.
Intuitively speaking our soundness proof is an extension of the one for EL but all subsumptions or disjointness
involving QCRs are based on QCR infeasibility tests performed by the ILP component. Once a subsumption or
disjointness has been proven, its evidence as an element of a node label becomes part of the saturation graph.
Since QCRs can interact with one another a QCR solution and its corresponding model is not proof enough for
a subsumption unless it is known to be the only possible solution. In order to test QCR-based entailment the
label sets LP and L¬P of potential (non-)subsumer nodes together with node labels are used for a feasibility test.
If such a set of QCRs has been proven to be infeasible, the corresponding subsumption or disjointness can be
added to the graph. Thus, only entailed subsumptions or disjointness will be inferred.
Lemma (Soundness). Let G be the saturation graph for a normalized Tbox T after the application of all satu-
ration rules in Figure 1 has terminated and C ∈ CAT and D ∈ CAT ∪ {⊥}, β ∈ {D, ¬D}.
˙ Then T |= C v β if it
holds that β ∈ L(vC ).
Proof. Let us assume that each rule application creates a new saturation graph and the sequence of rule applica-
¬
R,C I I
S G1 , . . . , Gm with Gi = (Vi , Ei , Li , LP i LP i ) and i ∈ 1..m. Let
tions until termination produce a sequence of graphs
F (x) = {y ∈ C | (x, y) ∈ R }, and Q(v, S) = hp,qi∈S {q | p ⊆ L(v)}. For all m ∈ N, models I of T , r ⊆ RT ,
and x ∈ C I we claim the following holds: (i) if β ∈ Lm (vC ) then T |= C v β; (ii) if r ⊆ Lm (vC , vq ), #vq ≥ n
I
then there exist yi ∈ ∆I with (x, yi ) ∈ R∈r RI , yi ∈ q0 ∈q q 0 , i ∈ 1..n.
T T
We prove our claim by induction on m. We start with m = 0 and assume that I is a model for T . For G0 we
have L0 (vC ) = {>, C}, L0 (vC , vD ) = ∅ implying that D = C. It is trivial to see that our claim holds. For the
induction step we make a case distinction according to applicable rules.
v-Rule Let φ ∈ Lm (vC ) \ Lm−1 (vC ) and x ∈ C I . Then there exists C ∈ Lm−1 (vC ) and C v φ ∈ T . Since I a
model of T it holds x ∈ φI .
v¬ -Rule Let ¬φ
˙ ∈ Lm (v) \ Lm−1 (v) and x ∈ ∆I \ C I . Then there exists ¬C ∈ Lm−1 (vC ) and φ v C ∈ T .
Since I a model of T it holds x ∈ ∆I \ φI .
v∗ -Rule Let τ ∈ Lm (v) \ Lm−1 (v) and x ∈ C I . Then there exists τ ∈ Lm−1 (vC ) and C I ⊆ τ I . Since I a model
of T it holds x ∈ τ I .
vu -Rule Let D ∈ Lm (v) \ Lm−1 (v) and x ∈ C1I , x ∈ C2I . Then there exists C1 , C2 ∈ Lm−1 (v) and C1 u C2 v
D ∈ T . Since I a model of T it holds x ∈ C1I ∩ C2I and thus x ∈ DI .
v¬ I I I
u -Rule Let ¬Cj ∈ Lm (v) \ Lm−1 (v) and x ∈ ∆ \ D , x ∈ Ci . Then there exists ¬D, Ci ∈ Lm−1 (v) and
Ci u Cj v D ∈ T . Since I a model of T it holds x ∈ Ci ∪ (∆I \ CjI ) ∪ (∆I \ DI ) and thus x ∈ ∆I \ CjI .
I
fil-Rule, e-Rule Let vq ∈ Vm \ Vm−1 , r ⊆ Lm (vC , vq ) such that q ⊆ Lm (vq ) and #vq ≥ n, Q = Lm−1 (vC ) ∩ CQ
T,
I
and let x ∈ q0 ∈Q q 0 . Due to the soundness and completeness of the ILP component and since I is
T
a model of T , w.l.o.g. we can assume that that a solution hr, q, ni ∈ σ(vC ) exists and we have yi with
I
(x, yi ) ∈ R∈r RI , yi ∈ q0 ∈q q 0 with i ∈ 1..n, and it holds ∀q 0 ∈ Q : x ∈ q 0I .
T T
I I I
⊥-Rule Let ⊥ ∈ Lm (vC ) \ Lm−1 (vC ), then either {A, ¬A} ⊆ Lm−1 (vT C ) and x ∈ A , x ∈ ∆ \ A or
I
infeasible(Lm−1 (vC )) and by the soundness of the ILP component x ∈ q∈Lm−1 (vC )∩CQ q . In both cases it
T
holds that x ∈ ⊥I .
119
P./ -Rule Let h{>}, {¬(./
˙ n R.C)}i ∈ LP m (vD ) \ LP m−1 (vD ). The newly created tuple is correct. Assume for a
node vF that ./ m R.E ∈ Lm−1 (vF ) and x ∈ F I . If the ILP component determines {./ m R.E, ¬(./ ˙ n R.C)}
as infeasible, then it holds x ∈ (./ m R.E)I , (./ m R.E)I ⊆ (./ n R.C)I ⊆ DI because I is a model of T
and ./ n R.C v D ∈ T .
¬
P./ -Rule Let h{>}, {./ n R.C}i ∈ LP m (vD ) \ LP m−1 (vD ). The newly created tuple is correct. Assume
for a node vF it holds ./ m R.E ∈ Lm−1 (vF ) and x ∈ F I . If the ILP component determines the set
{./ m R.E, ./ n R.C} as infeasible, then x ∈ (./ m R.E)I , ./ m R.E I ⊆ ∆I \ (./ n R.C)I ⊆ ∆I \ DI because
I is a model of T and D v ./ n R.C ∈ T .
P -Rule Let hp, qi ∈ LP m (vD ) \ LP m−1 (vD ), C I ⊆ DI , and w.l.o.g. let hp, qi ∈ LP m−1 (vC ). The newly created
tuple is correct because I is a model of T and a subsumption condition for C is also one for D since x ∈ C I
implies x ∈ DI .
P ¬ -Rule Let hp, qi ∈ L¬ ¬ I I
P m (vC ) \ LP m−1 (vC ), C ⊆ D , and w.l.o.g. let hp, qi ∈ LP m−1 (vD ). The newly created
tuple is correct because I is a model of T and a subsumption condition for ¬D is also one for ¬C since
x ∈ ∆I \ DI implies x ∈ ∆I \ C I .
Pu -Rule Let hp ∪ {Ci }, qi ∈ LP m (vD ) \ LP m−1 (vD ), and w.l.o.g. let hp, qi ∈ LP m−1 (vCj ). The newly created
tuple is correct because I is a model of T , Ci u Cj v D ∈ T , and if CiI ⊆ DI then a subsumption condition
for Cj is also one for D.
Rules vP1 , vP2 , vP3 , vP4 Let ⊥ ∈ Lm (v 0 ) \ Lm−1 (v 0 ), v 0 ∈ clone(vC , D), x ∈ C I . The rule vP1 added v 0 to Vk1 ,
the rules vP2 , vP3 fired
T at least once and added the corresponding QCRs to Lk2 (v 0 ) with k1 < k2 ≤ m−1. We
I I I
define QP (v) = ∆ \ q∈Q(v,LP (vD )) q as the domain complement of all QCRs contained in Q(v, LPm (vD ))
m
and QI (v) = q∈Lm (v)∩ CQ q I as the domain of all QCRs contained in Lm (v). W.l.o.g. we only consider the
T
T
case that infeasible(L(v 0 )) caused the unsatisfiability of v 0 . Due to the composition of Lm (v 0 ) and since I is
a model of T , it holds x ∈ QI (vC ), QI (vC ) ⊆ QIP (vC ) ⊆ DI .
The rules v¬ ¬ ¬ ¬
P1 , vP2 , vP3 , vP4 are analogous to vP1 , vP2 , vP3 , vP4 and for lack of space we omit this part of
the soundness proof here.
Lemma (Completeness). Let G be the saturation graph for a normalized Tbox T after the application of all
saturation rules in Figure 1 has terminated, and let A ∈ CAT , B ∈ CAT ∪ {⊥}, and β ∈ {B, ¬B}.
˙ Then,
β ∈ L(vA ), if T |= A v β.
Proof. We show the contrapositive. We assume that if D ∈ / L(vC ), then T |= C 6v D. In the following we show
that a model for C 6v D can be derived from the saturation graph G, i.e., by constructing a canonical model
I(C) w.r.t. T such that x ∈ C I \ DI . I(C) is defined iteratively starting with I(C0 ). We define ∆I0 (C) := {xC }
and DI0 (C) := {xC | D = C} for all D ∈ CAT .
v-Rule In case φ = D then for every x ∈ (∆Ii ∩ C Ii ) \ DIi+1 add x to DIi+1 . In case φ = ./ n R.C the model
construction is done in the fil- and e-Rule.
v¬ -Rule In case φ = D then for every x ∈ (∆Ii \ C Ii ) \ (∆Ii+1 \ DIi+1 ) add x to ∆Ii+1 \ DIi+1 . In case
φ = ./ n R.C the model construction is done in the fil- and e-Rule item below.
v∗ -Rule This rule has no impact on the model construction.
vu -Rule For every x ∈ (∆Ii ∩ C1Ii ∩ C2Ii ) \ DIi add x to DIi+1 .
v¬u -Rule For every x ∈ (∆
Ik
∩ CiIk ) \ (CjIk ∪ DIk ) add x to DIk+1 (i, j ∈ 1..2, i 6= j).
I
fil-Rule, e-Rule Let rIi = R∈r RIi , q Ii = q0 ∈q q 0 i , and k ∈ 1..n. For every x ∈ ∆Ii ∩ C Ii where no tuples
T T
I
(x, yk ) ∈ rIi+1 with yk ∈ q Ii+1 exist, introduce new individuals yk to ∆Ii+1 , for every q 0 ∈ q add yk to q 0 i+1 ,
and add (x, yk ) to RIi+1 for every R ∈ r.
Rules vP1 , vP2 , vP3 , vP4 Let QIPi = q∈Q(v,LP (vF )) q Ii , QIPi¬ = ∆Ii \ QIPi , QIv i = q∈Lv ∩ CQ q Ii , E, F ∈ CAT ,
T T
E T
and x ∈ E Ii . By the composition rules for LP and the infeasibility result of the ILP component we know
that E Ii ⊆ QIPi¬ ⊆ F Ii because E Ii ∩ QIPi = ∅. Now for every x ∈ (∆Ii ∩ E Ii ) \ F Ii+1 add x to F Ii+1 .
120
The rules v¬ ¬ ¬ ¬
P1 , vP2 , vP3 , vP4 are analogous to vP1 , vP2 , vP3 , vP4 and for lack of space we omit this part of
the completeness proof here.
The construction of a model is performed in a fair manner, i.e., every rule applicable to already existing
elements in ∆Ii is applied before applying rules to new elements. The constructed model I(C) is indeed a model
of C w.r.t T . Due to lack of space we cannot prove this in detail but we argue informally. Although our rules deal
with ELQ, a subset of these deal with EL if one assumes that only QCRs of the form ≥ 1R.C are allowed. Thus,
we claim that our rules are complete for EL. Due to the semantics of QCRs and their allowed occurrence on the
left- and and right-hand side of axioms, these can entail subsumptions that are not possible in EL. In order to
ensure completeness we introduced the labels LP and L¬ P that aggregate possible (non-)subsumption conditions
caused by QCRs. In order to prove subsumption or disjointness we create corresponding QCR clones. In case
a clone is satisfiable after all rules have terminated this clone can serve as a model for the non-subsumption
or non-disjointness. In case additional entailed information is added to the saturation graph that causes the
unsatisfiability of a QCR clone, we will add the entailed subsumption or disjointness to the sets subs and
unsat that are used by the ILP component. Regarding the fil- and e-rule there could exist another possible
incompleteness because a numerically satisfiable set of QCRs could eventually cause the unsatisfiability of a
created anonymous node due to entailed information missing in the graph at the time of the feasibility test.
However, if such an anonymous node becomes unsatisfiable, the cause of unsatisfiability is learned by adding its
cause to the sets subs and unsat. This ensures that a previously computed solution is monotonically constrained
until either an anonymous node is determined as satisfiable or the set of QCRs becomes eventually infeasible.
Again, this ensures that no model for non-subsumption or non-disjointness is overlooked and no subsumption or
disjointness is missed.
Lemma (Termination). For every normalized ELQ Tbox over CT and RT the application of the saturation rules
in Figure 1 will terminate in finite time.
Proof. The algorithm terminates naturally because the saturation graph is finite and its number of nodes is
bounded by the size of the power set of CT and RT respectively, cycles are avoided by reusing nodes in accordance
to standard subset blocking. Finally, the number of concepts, edges, QCRs, and subsumption tuples that can
be added to L, LP , and L¬ P is again bounded by the size of the power set of CT and RT respectively. All rules
extend labels monotonically. Once the precondition of a rule is true for elements of a graph G and the rule has
fired, it cannot fire again for the same set of elements, thus, any series of rule applications is finite.
6 A First Experimental Evaluation
We developed a prototype system called Avalanche that implements our calculus as proof of concept.2 Its ILP
component is based on IBM ILOG CPLEX Optimization Studio [IBM] that is freely available for academic
research. Avalanche currently parses only ELQ ontologies expressed in RDF/XML syntax. For this first release
our focus is on a sound, complete, and terminating implementation. We did not optimize Avalanche for EL
ontologies yet and many of our saturation rules are implemented very inefficiently. Deciding subsumption for
named concepts where LP and/or L¬ P are not empty is currently computed very naively. We generate a QCR
clone for each possible subsumption or disjointness via QCRs and the number of clones is bounded by n2 if the
Tbox contains n named concepts.
Avalanche has been written in the Java programming language. It consists of two main components: a
reasoner and an external ILP module. The ILP module is needed for feasibility testing of QCRs. The reasoner
executes in the following way: First, it parses the input ontology file. The axioms in the file must conform to
our ELQ syntax. If an axiom in the ontology does not conform to the ELQ syntax restrictions an exception will
be raised and the system will terminate. After the parsing is completed, the input axioms are rewritten to our
internal normal form. Then, we build nodes representing all concepts declared in the original ontology file as
well as the ones obtained during the normalization phase.
Our reasoning process is divided into two phases: an unfolding and a rule application phase. During the
unfolding phase we apply the rules v, v./ , v¬ ¬
./ , P , and P . In this phase, each rule is applied only once to each
node. Afterwards, during the rule application phase, we apply all rules rules except v, v./ , and v¬ ./ . The rules
do not have to be applied in any particular order. We apply all matching rules to all the nodes. The system
calls the external ILP module when it needs to solve a system of inequalities.
2 Avalanche web page: https://users.encs.concordia.ca/%7Ehaarslev/Avalanche/
121
Ontology Name #Axioms #Concepts #Roles #QCRs
canadian-parliament-factions-1 48 21 6 19
canadian-parliament-factions-2 56 24 7 25
canadian-parliament-factions-3 64 27 8 30
canadian-parliament-factions-4 72 30 9 35
canadian-parliament-factions-5 81 34 10 40
canadian-parliament-full-factions-1 51 22 6 22
canadian-parliament-full-factions-2 60 25 7 30
canadian-parliament-full-factions-3 69 28 8 36
canadian-parliament-full-factions-4 78 31 9 42
canadian-parliament-full-factions-5 87 34 10 48
C-SAT-exp-ELQ 26 10 4 13
C-UnSAT-exp-ELQ 26 10 4 13
genomic-cds rules-ELQ-fragment-1 716 358 1 357
genomic-cds rules-ELQ-fragment-2 718 359 1 357
Figure 3: Metrics of ELQ benchmark ontologies (#=Number of . . . )
The experiments were performed on a MacBook Pro (2.6 GHz Intel Core i7 processor, 16GB memory) using
only one core. The comparison results (average of 3 runs) are shown in Figure 4. We compared Avalanche with
major OWL reasoners: FaCT++ (1.6.4) [FaC], HermiT (1.3.8) [Her], Konclude (0.6.2) [Kon], and Racer (3.0)
[HM01, HHMW12, Rac], which is the only other available OWL reasoner using an ILP component for reasoning
about QCRs. The algorithms implementing Racer’s ILP component are in general best-case exponential to the
number of QCRs given for one concept. Some metrics about the benchmark ontologies are shown in Figure 3.
The first benchmark (see top part of Figure 4) uses variants of two real-world ontologies modelling a component
of the Canadian Parliament, namely the House of Commons, which is a democratically elected body that had 308
members in the last Parliament (most members elected in 2011) [Can]. For each Canadian province a faction is
defined [Can] that is composed of members elected in the same province. In order to ensure subsumptions based
on QCRs we defined four concepts categorizing factions as tiny, small, medium, or big, based on the number
of faction members. Each faction belongs to exactly one of these faction categories. The second version adds a
concept defining for the House of Commons the number of members from each province [Can]. The only reasoners
that can classify all variants of the simplest of these ontologies within the given time limit are Avalanche and
Racer. Avalanche still exhibits an exponential runtime increase but it is the only reasoner that can classify
all variants of these ontologies. The performance of Racer for the simpler ontology is a good indication that
Avalanche can achieve similar runtimes with optimized reasoning algorithms.
The second benchmark (see middle part of Figure 4) uses synthetic concept templates that are similar to
the example used in Section 3. The original ALCQ concepts are shown below the table. They were manually
rewritten into normalized ELQ as demonstrated in Section 3. The concept templates use a variable n that is
increased exponentially. The numbers used in the template are bounded by the value of 2n. The first template
is satisfiable and the second one unsatisfiable. Only Avalanche and Racer can classify all variants of these small
ontologies within the time limit.
The third benchmark (see bottom part of Figure 4) uses two ELQ fragments of a real world ontology, genomic-
cds rules [Sam13, Sam14], which was developed for pharmacogenetics and clinical decision support. It contains
many concepts using QCRs of the form = 2 has.Ai . However, in these fragments the concepts (Ai ) occurring in
the qualification of the QCRs do not interact with one another. This simplifies the reasoning and all reasoners
except Racer perform well. Avalanche and HermiT as well as FaCT++ and Konclude have similar runtimes.
These fragments are interesting because the concept <#human> contains several hundred QCRs using the same
role. This is one of the reasons why Racer timed out for both fragments.
7 Summary
We presented the first calculus that combines saturation and ILP-based reasoning to decide subsumption for
ELQ. Our preliminary experiments indicate that this calculus offers a better scalability for qualified cardinality
restrictions than approaches combining both tableaux and ILP as well as traditional (hyper)tableau methods.
We already started to improve the efficiency of our implementation and expect a significant speedup for our next
122
Canadian Parliament Factions only Canadian Parliament Full
#F Ava Fac Her Kon Rac Ava Fac Her Kon Rac
5 11.1 TO TO TO 0.12 375 TO TO TO TO
4 8.4 TO TO TO 0.11 22.4 TO TO TO TO
3 2.7 TO TO TO 0.07 4.1 TO TO TO TO
2 1.4 TO TO TO 0.07 2.7 TO TO TO 10.5
1 0.8 TO TO 7.3 0.05 1.1 TO TO TO 0.44
C-SAT-exp-ELQ C-UnSAT-exp-ELQ
n Ava Fac Her Kon Rac Ava Fac Her Kon Rac
40 0.69 TO TO TO 0.01 0.63 TO TO TO 0.01
20 0.62 TO TO TO 0.01 0.80 TO TO TO 0.01
10 0.63 TO TO TO 0.01 0.99 TO TO TO 0.01
5 0.72 6.3 4.4 0.91 0.01 0.74 TO TO 784 0.01
3 0.62 0.17 0.18 0.33 0.01 0.75 0.25 1.15 1.18 0.01
Sat: C v (≤ n R.¬A t ≤ n−1 R.¬B) u ≥ 2n R.> u ≤ n R.A u ≤ n R.B
Unsat: C v (≤ n−1 R.¬At≤ n−1 R.¬B)u≥ 2n R.>u≤ n R.Au≤ n R.B
Satisfiability of concept <#human>
Name Ava Fac Her Kon Rac
genomic-cds rules-ELQ-fragment-1 1.13 27.7 0.87 27.7 TO
genomic-cds rules-ELQ-fragment-2 2.4 28.2 1.14 28.3 TO
Figure 4: Benchmark runtimes in seconds with a timeout of 1000 seconds (TO=timeout, #F=Number of Factions,
Ava=Avalanche, Fac=FaCT++, Her=HermiT, Kon=Konclude, Rac=Racer)
release. We plan to add a preprocessing phase that automatically rewrites ALCQ ontologies to our ELQ syntax.
Our next steps are to extend our calculus to cover role hierarchies and inverse roles.
References
[ADF09] H. M. B. Amor, J. Desrosiers, and A. Frangioni. On the choice of explicit stabilizing terms in column
generation. Discrete Applied Mathematics, 157(6):1167–1184, 2009.
[BBL05] F. Baader, S. Brandt, and C. Lutz. Pushing the EL envelope. In Proc. of IJCAI, pages 364–369,
2005.
[BJN+ 98] C. Barnhart, E. L. Johnson, G. L. Nemhauser, M. W. P. Savelsbergh, and P. H. Vance. Branch-and-
price: Column generation for solving huge integer programs. Operations Research, 46(3):316–329,
1998.
[BMC+ 16] A. Bate, B. Motik, B. Cuenca Grau, F. Simančı́k, and I. Horrocks. Extending consequence-based
reasoning to SRIQ. In Proc. of KR, pages 187–196, 2016.
[Can] Canadian Parliament. https://en.wikipedia.org/wiki/House of Commons of Canada.
[Chv83] V. Chvatal. Linear Programming. Freeman, 1983.
[DDS11] G. Desaulniers, J. Desrosiers, and S. Spoorendonk. Cutting planes for branch-and-price algorithms.
Networks, 58:301–310, 2011.
[DGL14] J. Desrosiers, J. Gauthier, and M. Lübbecke. Row-reduced column generation for degenerate master
problems. European Journal of Operational Research, 236:453–460, July 2014.
[DW60] G. B. Dantzig and P. Wolfe. Decomposition principle for linear programs. Operations research,
8(1):101–111, 1960.
[FaC] FaCT++. http://owl.cs.manchester.ac.uk/tools/fact/.
123
[FH10a] J. Faddoul and V. Haarslev. Algebraic tableau reasoning for the description logic SHOQ. Journal
of Applied Logic, 8(4):334–355, 2010.
[FH10b] J. Faddoul and V. Haarslev. Optimizing algebraic tableau reasoning for SHOQ: First experimental
results. In Proc. of DL, pages 161–172, 2010.
[FH10c] N. Farsiniamarj and V. Haarslev. Practical reasoning with qualified number restrictions: A hybrid
Abox calculus for the description logic SHQ. AI Communications, 23(2-3):334–355, 2010.
[GG61] P. C. Gilmore and R. E. Gomory. A linear programming approach to the cutting-stock problem.
Operations research, 9(6):849–859, 1961.
[HB91] B. Hollunder and F. Baader. Qualifying number restrictions in concept languages. In Proc. of KR,
pages 335–346, 1991.
[Her] HermiT. http://www.hermit-reasoner.com/download.html.
[HHMW12] V. Haarslev, K. Hidde, R. Möller, and M. Wessel. The RacerPro knowledge representation and
reasoning system. Semantic Web, 3(3):267–277, 2012.
[HM01] V. Haarslev and R. Möller. RACER system description. In Proc. of IJCAR, pages 701–705, 2001.
[IBM] IBM. https://www.ibm.com/developerworks/downloads/ws/ilogcplex/.
[Kaz09] Y. Kazakov. Consequence-driven reasoning for horn SHIQ ontologies. In Proc. of IJCAI, pages
2040–2045, 2009.
[Kon] Konclude. http://www.derivo.de/en/produkte/konclude/.
[Las70] L. Lasdon. Optimization Theory for Large Systems. MacMillan, New York, 1970.
[LD05] M. Lübbecke and J. Desrosiers. Selected topics in column generation. Operations Research, 53:1007–
1023, 2005.
[Meg87] N. Megiddo. On the complexity of linear programming. In Advances in Economic Theory, pages
225–268. Cambridge University Press, 1987.
[NW88] G. L. Nemhauser and L. A. Wolsey. Integer and Combinatorial Optimization. Wiley, New York,
1988.
[NW99] G. Nemhauser and L. Wolsey. Integer and Combinatorial Optimization. Wiley, 1999. reprint of the
1988 edition.
[OK99] H. Ohlbach and J. Köhler. Modal logics, description logics and arithmetic reasoning. Artificial
Intelligence, 109(1-2):1–31, 1999.
[Rac] Racer. https://www.ifis.uni-luebeck.de/index.php?id=385.
[RH12] L. Roosta Pour and V. Haarslev. Algebraic reasoning for SHIQ. In Proc. of DL, pages 530–540,
2012.
[Sam13] M. Samwald. Genomic CDS: an example of a complex ontology for pharmacogenetics and clinical
decision support. In 2nd OWL Reasoner Evaluation Workshop, pages 128–133. CEUR, 2013.
[Sam14] M. Samwald. An update on genomic CDS, a complex ontology for pharmacogenomics and clinical
decision support. In 3rd OWL Reasoner Evaluation Workshop, pages 58–63. CEUR, 2014.
[SGL14] A. Steigmiller, B. Glimm, and T. Liebig. Coupling tableau algorithms for expressive description
logics with completion-based saturation procedures. In Proc. of IJCAR, pages 449–463, 2014.
[SMH14] F. Simančı́k, B. Motik, and I. Horrocks. Consequence-based and fixed-parameter tractable reasoning
in description logics. Artificial Intelligence, 209:29–77, 2014.
[Van11] F. Vanderbeck. Branching in branch-and-price: a generic scheme. Mathematical Programming,
130(2):249–294, 2011.
124