=Paper=
{{Paper
|id=Vol-2211/paper-15
|storemode=property
|title=Handling Nominals and Inverse Roles using Algebraic Reasoning
|pdfUrl=https://ceur-ws.org/Vol-2211/paper-15.pdf
|volume=Vol-2211
|authors=Humaira Farid,Volker Haarslev
|dblpUrl=https://dblp.org/rec/conf/dlog/FaridH18
}}
==Handling Nominals and Inverse Roles using Algebraic Reasoning==
https://ceur-ws.org/Vol-2211/paper-15.pdf
Handling Nominals and Inverse Roles using
Algebraic Reasoning
Humaira Farid and Volker Haarslev
Concordia University, Montreal
h_arid@encs.concordia.ca, haarslev@cse.concordia.ca
Abstract. This paper presents a novel SHOI tableau calculus which
incorporates algebraic reasoning for deciding ontology consistency. Nu-
merical restrictions imposed by nominals, existential and universal re-
strictions are encoded into a set of linear inequalities. Column generation
and branch-and-price algorithms are used to solve these inequalities. Our
preliminary experiments indicate that this calculus performs better on
SHOI ontologies than standard tableau methods.
1 Introduction and Motivation
Description Logic (DL) is a formal knowledge representation language that is
used for modeling ontologies. Modern description logic systems provide reason-
ing services that can automatically infer implicit knowledge from explicitly ex-
pressed knowledge. Designing reasoning algorithms with high performance has
been one of the main concerns of DL researchers. One of the key features of
many description logics is support for nominals. Nominals are special concept
names that must be interpreted as singleton sets. They allow to use Abox in-
dividuals within concept descriptions. However, nominals carry implicit global
numerical restrictions that increase reasoning complexity. Moreover, the inter-
action between nominals and inverse roles leads to the loss of the tree model
property. Most state-of-the-art reasoners, such as Konclude [23], Fact++ [24],
HermiT [21], have implemented traditional tableau algorithms. Konclude also
incorporated consequence-based reasoning into its tableau calculus [22]. These
reasoners try to construct completion graphs in a highly non-deterministic way
in order to handle nominals. For example, a small ALCO ontology models
Canada consisting of its ten provinces: CA_Province ≡ {Ontario, Quebec,
NovaScotia, NewBrunswick , Manitoba, BritishColumbia, PrinceEdwardIsland ,
Saskatchewan, NewfoundlandAndLabrador , Alberta}. If one tries to model that
Canada consists of 11 provinces, it is trivial to see that it is not possible be-
cause the cardinality of CA_Province is implicitly restricted to the 10 provinces
listed as nominals. However, according to our preliminary experiments, above
mentioned DL reasoners are unable to decide this inconsistency within a rea-
sonable amount of time. Consequence-based (CB) reasoning algorithms are also
extended to more expressive DLs such as SHOI [6] and SROIQ [7]. Since their
implementations are not available, we could not analyze these reasoners.
However, algebraic DL reasoners are considered more efficient in handling
numerical restrictions [10,13,14,25]. RacerPro [14] was the first highly optimized
reasoner that combined tableau-based reasoning with algebraic reasoning [15].
Other tableau-based algebraic reasoner for SHQ [13], SHIQ [20], SHOQ [11,10]
are also proposed to handle qualified number restrictions (QNRs) and their in-
teraction with inverse roles or nominals. These reasoners use an atomic decom-
position technique to encode number restrictions into a set of linear inequalities.
These inequalities are then solved by integer linear programming (ILP). These
reasoners perform very efficiently in handling huge values in number restrictions.
However, their ILP algorithms are best-case exponential to the number of in-
equalities. For example, in case of m inequalities they require 2m variables in
order to find the optimal solution. However, for ILP with a huge number of
variables it is not feasible to enumerate all variables. To overcome this problem,
the column generation technique has been used [25,27] which considers a small
subset of variables. However, to the best of our knowledge, no algebraic calculus
can handle DLs supporting nominals and inverse roles simultaneously.
In this paper, we present a novel algebraic tableau calculus for SHOI to
handle a large number of nominals and their interaction with inverse roles. The
rest of this paper is structured as follows. Section 2 defines important terms and
introduces SHOI. Section 3 presents the algebraic tableau calculus for SHOI.
Section 4 provides evaluation results for the implemented prototype Cicada. The
last section concludes our paper. An extended version of this paper [12] contains
more details about ILP and the example presented in Section 3.3.
2 Preliminaries
In this section, we introduce SHOI and some notations used later. Let N =
NC ∪ No where NC represents concept names and No nominals. Let NR be a set
of role names with a set of transitive roles NR+ ⊆ NR . The set of roles in SHOI
is NR ∪ {R− | R ∈ NR } where R− is called the inverse of R. A function Inv
returns the inverse of a role such that Inv(R) = R− if R ∈ NR and Inv(R) = S
if R = S − and S ∈ NR . An interpretation I = (∆I , ·I ) consists of a non-empty
set ∆I of individuals called the domain of interpretation and an interpretation
function ·I . Table 1 presents syntax and semantic of SHOI. We use > (⊥) as
an abbreviation for A t ¬A (A u ¬A) for some A ∈ NC . In the following ]{.}
denotes set cardinality.
A role inclusion axiom (RIA) of the form R v S is satisfied by I if RI ⊆ S I .
We denote with v∗ the transitive, reflexive closure of v over NR . If R v∗ S, we
call R a subrole of S and S a superrole of R. A general concept inclusion (GCI)
C v D is satisfied by I if C I ⊆ DI . A role hierarchy R is a finite set of RIAs.
A Tbox T is a finite set of GCIs. A Tbox T and its associated role hierarchy R
is satisfied by I (or consistent) if each GCI and RIA is satisfied by I. Such an
interpretation I is then called a model of T . A concept description C is said to be
satisfiable by I iff C I 6= ∅. An Abox A is a finite set of assertions of the form a : C
(concept assertion) with aI ∈ C I , and (a, b) : R (role assertion) with (aI , bI ) ∈
RI . Due to nominals, a concept assertion a : C can be transformed into a concept
inclusion {a} v C and a role assertion (a, b) : R into {a} v ∃R.{b}. Therefore,
concept satisfiability and Abox consistency can be reduced to Tbox consistency
Table 1. Syntax and semantics of SHOI
Construct Syntax Semantics
atomic concept A AI ⊆ ∆I
negation ¬C ∆I \ C I
conjunction C uD C I ∩ DI
disjunction C tD C I ∪ DI
value restriction ∀R.C {x ∈ ∆I | ∀y : (x, y) ∈ RI ⇒ y ∈ C I }
exists restriction ∃R.C {x ∈ ∆I | ∃y ∈ ∆I : (x, y) ∈ RI ∧ y ∈ C I }
nominal {o} ]{o}I = 1
role R RI ⊆ ∆I × ∆I
−
inverse role R (R− )I = {(y, x) | (x, y) ∈ RI }
transitive role R ∈ NR+ (x, y) ∈ RI ∧ (y, z) ∈ RI ⇒ (x, z) ∈ RI
by using nominals. We use {o1 , . . . , on } as an abbreviation for {o1 } t · · · t {on }
and may write {o} as o. Moreover, we do not make the unique name assumption;
therefore, two nominals might refer to the same individual.
Nominals carry implicit global numerical restrictions. For example, if C v
{o1 , o2 , o3 } (or {o1 , o2 , o3 } v C), then o1 , o2 , o3 impose a numerical restriction
that there can be at most (or at least, if o1 , o2 , o3 ∈ No are declared as pair-
wise disjoint) three instances of C. These restrictions are global because they
affect the set of all individuals of C in ∆I . These implicit numerical restrictions
increase reasoning complexity.
3 An Algebraic Tableau Calculus for SHOI
In this section, we present an algebraic tableau calculus for SHOI that decides
Tbox consistency. Since nominals carry numerical restrictions, algebraic reason-
ing is used to ensure their semantics. The algorithm takes a SHOI Tbox T
and its role hierarchy R as input and tries to create a complete and clash-free
completion graph in order to check Tbox consistency. The reasoner is divided
into two modules: 1) Tableau Module (TM), and 2) Algebraic Module (AM).
Let G = (V, E, L, B) be a completion graph for a SHOI Tbox T where V
is a set of nodes and E a set of edges. Each node x ∈ V is labelled with a set
of concepts L(x), and each edge hx, yi ∈ E with a set of role names L(x, y). For
each node x ∈ V , if L(x) contains a universal restriction on role R and there
exists an R-neighbour of x, then B(x) contains a tuple of the form hv, L(x, v)i
where v ∈ V is an R-neighbour of x. We use ]v to denote the cardinality of a
node v. For convenience, we assume that all concept descriptions are in negation
normal form.
TM starts with some preprocessing and reduces alldthe concept axioms in
a Tbox T to a single axiom > v CT such that CT := CvD∈T nnf (¬C t D),
where nnf transforms a given concept expression to its negation normal form.
The algorithm checks consistency of T by testing the satisfiability of o v CT
where o ∈ No is a fresh nominal in T , which means that at least oI ∈ CT I
and CT I 6= ∅. Moreover, since >I = ∆I then every domain element must
also satisfy CT . For creating a complete and clash-free completion graph, TM
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) ∪ {C} for some C ∈ {C1 , C2 }
∀-Rule if ∀S.C ∈ L(x) and there ∃y with R ∈ L(x, y), C ∈ / L(y) and R v∗ S
then set L(y) = L(y) ∪ {C}
∀+ -Rule if ∀S.C ∈ L(x) and there exist U, R with R ∈ NR+ and U v∗ R,
R v∗ S, and a node y with U ∈ L(x, y) and ∀R.C ∈ / L(y)
then set L(y) = L(y) ∪ {∀R.C}
nommerge -Rule if for some o ∈ No there are nodes x, y with o ∈ L(x) ∩ L(y), x 6= y
then if x is an initial node, then merge y into x, else merge x into y
inverse-Rule if ∀R− .C ∈ L(y), R ∈ L(x, y), and hx, L(y, x)i ∈ / B(y)
then set B(y) = B(y) ∪ {hx, L(y, x)i}
fil -Rule if hR, C, n, Vi ∈ σ(x) and x is not blocked then
1. if V = ∅ and there exists no R-neighbour y of x with C ⊆ L(y),
]y ≥ n, then create a new node y with L(y) ← C and ]y ← n
2. else for all v ∈ V add C to L(v) and set ]v = n
e-Rule if hR, C, n, Vi ∈ σ(x) and C ⊆ L(y), ]y ≥ n, R * L(x, y)
then merge R into L(x, y) and {Inv(R) | R ∈ R} into L(y, x), and
for all S with R v∗ S ∈ R add S to L(x, y) and Inv(S) to L(y, x)
Fig. 1. The expansion rules for SHOI
applies expansion rules (see Figure 1 and Section 3.1). AM handles all numerical
restrictions using ILP. It generates inequalities and solves them using the branch-
and-price technique (see Section 3.2 for details). We use equality blocking [18,16]
due to the presence of inverse roles.
3.1 Expansion Rules
In order to check the consistency of a Tbox T , the proposed algorithm creates a
completion graph G using the expansion rules shown in Figure 1. A node x in G
contains a clash if {A, ¬A} ⊆ L(x) for A ∈ NC or AM has no feasible solution
for x. G is complete if no expansion rule is applicable to any node in G. T is
consistent if G is complete and no node in G contains a clash.
The u-Rule, t-Rule and ∀-Rule are similar to standard tableau expansion
rules for ALC. The ∀+ -Rule preserves the semantics of transitive roles. The
nommerge -Rule merges two nodes containing in their label the same nominal.
Suppose there is o ∈ L(x) and o ∈ L(y), and nodes x and y are not the same,
then nommerge -Rule merges x into y. It adds L(x) to L(y) and moves all edges
leading to (from) x so that they lead to (from) y. For each node z, if hz, yi ∈ E
and hz, xi ∈ E, then L(z, y) = L(z, y) ∪ L(z, x). Similarly, if hy, zi ∈ E and
hx, zi ∈ E, then L(y, z) = L(y, z) ∪ L(x, z). It also merges B(x) into B(y).
If L(x, y) = {R} and ∀R− .C ∈ L(y), then the inverse-Rule encodes for AM
the already existing R− -edge by adding a tuple hx, {R− }i to B(y). AM plays
also an important role if nominals occur in universal restriction. For example,
consider the axioms A v ∃R.B, B v ∃R− .Cu∃R− .Du∀R− .{o1 , o2 } and o1 uo2 v
⊥, where A, B, C, D ∈ NC , o1 , o2 ∈ No and R ∈ NR . Suppose we have A ∈
L(x), R ∈ L(x, y) and B ∈ L(y). Since nominals carry numerical restrictions,
∀R− .{o1 , o2 } implies that we can have at most 2 R− -neighbours of y. However,
standard tableau reasoners might create two new R− -neighbours of y without
considering the existing R− -neighbour x of y. Then they try to merge these three
nodes in a non-deterministic way to satisfy the numerical restriction imposed
by nominals. In our approach, the inverse-Rule encodes information about an
existing R− -neighbour of y and AM generates a deterministic solution.
For a node x, AM transforms all existential restrictions, universal restrictions
and nominals to a corresponding system of inequalities. AM then processes these
inequalities and gives back a solution set σ(x). The set σ(x) is either empty or
contains solutions derived from feasible inequalities. In case of infeasibility AM
signals a clash. A solution is defined by a set of tuples of the form hR, C, n, Vi with
R ⊆ NR , C ⊆ N , n ∈ N, n ≥ 1 and V ⊆ V . Each tuple represents n R-neighbours
of x (where R is a set of roles) that are instances of all elements of C. Here, V
is an optional set that contains existing R-neighbours of x that must be reused
and C is added to their labels. Consider the axiom A v ∃R.B u ∃R.C u ∀S. {o},
where A, B, C ∈ NC , o ∈ No , R, S ∈ NR , R v S, and A ∈ L(x). AM returns
the solution σ(x) = {h{R, S}, {B, C, o}, 1i}. The fil -Rule is used to generate
nodes based on the arithmetic solution that satisfies a set of inequalities. For
the above solution, the fil -Rule creates one node y with cardinality 1 such that
L(y) ← {B, C, o} and ]y = 1. The e-Rule creates an edge between nodes x
and y, and adds R, S to L(x, y) and Inv(R), Inv(S) to L(y, x). The e-Rule always
adds all implied superroles to edge labels.
3.2 Generating Inequalities
Dantzig and Wolfe [8] proposed a column generation technique for solving linear
programming (LP) problems, called Dantzig–Wolfe decomposition, where a large
LP is decomposed into a master problem and a subproblem (or pricing problem).
In case of LP problems with a huge number of variables, column generation works
with a small subset of variables and builds a Restricted Master Problem (RMP).
The Pricing Problem (PP) generates a new variable with the most reduced
cost if added to RMP (see [4,26] for details). However, column generation may
not necessarily give an integral solution for an LP relaxation, i.e., at least one
variable has not an integer value. Therefore, the branch-and-price method [3]
has been used which is a combination of column generation and branch-and-
bound technique [9]. We employ this technique by mapping number restrictions
to linear inequality systems using a column generation ILP formulation (see [26]
for details). CPLEX [5] has been used to solve our ILP formulation.
Encoding Existential Restrictions and Nominals into Inequalities The
atomic decomposition technique [19] is used to encode numerical restrictions
on concepts and role fillers into inequalities. These inequalities are then solved
for deciding the satisfiability of the numerical restrictions. The existential re-
strictions are converted into ≥ 1 inequalities. The cardinality of a partition
element containing a nominal o is equal to 1 due to the nominal semantics;
]{o}I = 1 for each nominal o ∈ No . Therefore, the decomposition set is defined
as Q = Q∃ ∪ Q∀ ∪ Qo , where Q∃ (Q∀ ) contains existential (universal) restrictions
Fig. 2. Overview of the algebraic reasoning process
and Qo contains all related nominals. Each element Rq ∈ Q∃ ∪ Q∀ represents a
role R ∈ NR and its qualification concept expression q and each element Iq ∈ Qo
represents a nominal q ∈ No . The elements in Q∀ are used by AM to ensure
the semantics of universal restrictions. The set of related nominals Qo ⊆ No is
defined as Qo = {o | o ∈ clos(q) ∧ Rq ∈ Q∃ ∪ Q∀ } where clos(q) is the closure of
concept expression q. The atomic decomposition considers all possible ways to
decompose Q into sets that are semantically pairwise disjoint.
Branch-and-Price Method In the following, we use a Tbox T and its role
hierarchy R, a completion graph G, a decomposition set Q and a partitioning
P that is the power set of Q containing all subsets of Q except the empty set.
Each partition element p ∈ P represents the intersection of its elements. We
decompose our problem into two subproblems: (i) restricted master problem
(RMP), and (ii) pricing problem (PP). RMP contains a subset of columns and
PP computes a column that can maximally reduce the cost of RMP’s objective.
Whenever a column with negative reduced cost is found, it is added to RMP.
Number restrictions are represented in RMP as inequalities, with a restricted
set of variables. The flowchart in Figure 2 illustrates the whole process.
Restricted Master Problem RMP is obtained by considering only variables
xp with p ∈ P 0 and P 0 ⊆ P and relaxing the integrality constraints on the xp
variables. Initially P 0 is empty and RMP contains only artificial variables h to
obtain an initial feasible inequality system. Each artificial variable corresponds
to an element in Q∃ ∪Qo such that hRq , Rq ∈ Q∃ and hIq , Iq ∈ Qo . An arbitrarily
large cost M is associated with every artificial variable. If any of these artificial
variables exists in the final solution, then the problem is infeasible. The objective
of RMP is defined as the sum of all costs as shown in (1) of the RMP below.
X X X
Min costp xp + M hRq + M hIq subject to (1)
p∈P 0 Rq ∈Q∃ Iq ∈Qo
X
aR
p xp + hRq ≥ 1 Rq ∈ Q∃
q
(2)
p∈P 0
X
aIpq xp + hIq = 1 Iq ∈ Qo (3)
p∈P 0
xp ∈ R+ with p ∈ P 0 (4)
aR Iq +
p , ap ∈ {0, 1}, hRq , hIq ∈ R with Rq ∈ Q∃ , Iq ∈ Qo
q
where a decision variable xp represents the elements of the partition element p ∈
R
P 0 . The coefficients ap are associated with variables xp and ap q indicates whether
I
an R-neighbour that is an instance of q exists in p. Similarly, apq indicates
whether a nominal q exists in p. The weight costp defines the cost of selecting
p and it depends on the number of elements p contains. Since we minimize the
objective function, costp in the objective (1) ensures that only subsets with
entailed concepts will be added which are the minimum number of concepts
that are needed to satisfy all the axioms. Constraint (2) encodes existential
restrictions and (3) numerical restrictions imposed by nominals (i.e., ]{o}I = 1).
Constraint (4) states the integrality condition relaxed from xp ∈ Z+ to xp ∈ R+ .
Pricing Problem: The objective of PP uses the dual values π, ω as coefficients
of the variables that are associated with a potential partition element. The binary
variables rRq , rIq , bq (q ∈ N ) are used to ensure the description logic semantics.
A binary variable rR> is used to handle role hierarchy. A variable bq is set to
1 if there exists an instance of concept q and rRq is set to 1 if there exists an
R-neighbour that is an instance of concept q. Likewise, rIq is set to 1 if there
exists a nominal q. Otherwise these variable are set to 0. The PP is given below.
X X X
Min bq − πRq rRq − ωIq rIq subject to (5)
q∈N Rq ∈Q∃ Iq ∈Qo
rRq − bq ≤ 0 Rq ∈ Q∃ , R ∈ NR , q ∈ NC (6)
rIq − bq = 0 Iq ∈ Qo , q ∈ No (7)
rRq − rR> ≤ 0 R ∈ NR , q ∈ N (8)
rR> − bq ≤ 0 Rq ∈ Q∀ , R ∈ NR , q ∈ N (9)
rR> − rS> ≤ 0 R v S ∈ R, R, S ∈ NR (10)
bq , rRq , rIq , rR> , rS> ∈ {0, 1}
where vector π and ω are dual variables associated with (2) and (3) respectively.
For each at-least restriction represented in (2), Constraint (6) is added to PP,
which ensures that if rRq = 1 then variable for bq must exist in P 0 . Similarly,
(7) ensures the semantics of nominals represented in (2). Constraints (8) - (10)
ensure the semantics of universal restrictions and role hierarchies respectively.
We can also map the semantics of selected DL axioms, where only atomic
concepts occur, into inequalities, as shown in Table 2. For every T |= A u B v C,
AM adds bA +bB −1 ≤ bC to PP. Therefore, if PP generates a partition containing
A and B, then it must also contain C. Similarly, for every T |= A v B t C, AM
adds bA ≤ bB + bC to PP. This inequality ensures that if a partition contains A,
then it must also contain B or C.
Soundness and Completeness of Algebraic Module All existential restric-
tions and nominals are converted into linear inequalities and added to RMP.
Table 2. DL axioms and their corresponding PP inequalities (n ≥ 1)
DL Axiom Inequality in PP Description
Pn If a set contains A1 , ..., An , then it
A1 u ... u An v B i=1 bAi − (n − 1) ≤ bB also contains B.∗
If a set contains A, then it also
bA ≤ n
P
A v B1 t ... t Bn i=1 bBi contains at least one concept from
B1 , ..., Bn .
∗
Encodes unsatisfiability and disjointness in case B v∗ ⊥
Other axioms, such as universal restrictions, role hierarchy, subsumption and
disjointness, are embedded in PP. In case of feasible inequalities, the branch-
and-price algorithm returns a solution set that contains valid partition elements.
Since the branch-and-price algorithm satisfies all the axioms embedded in RMP
and PP, this solution is sound. Moreover, it is also complete because CPLEX is
used to solve linear inequalities and it does not overlook any possible solution.
Proposition 1. For a set of inequalities, the arithmetic module either generates
an optimal solution which satisfies all inequalities or detects infeasibility.
3.3 Example Illustrating Rule Application and ILP formulation
Consider the small Tbox
A v ∃R.B u ∃R.{o1}
B u {o1} v ⊥
B v ∃R.C u ∃R− .D u ∀S − .{o2}
C uD v⊥
C v ∃R.E
E v ∀S − . {o1}
with NR = {R, S}, {A, B, C, D, E} ⊆ NC , {o1, o2} ⊆ No , and R v S ∈ R. For
the sake of better readability, we apply in this example lazy unfolding [2,17].
1. We start with root node x and its label L(x) = {A} and by unfolding A and
applying the u-Rule we get L(x) = {A, ∃R.B, ∃R.{o1}}.
2. Since {∃R.B, ∃R.{o1}} ⊆ L(x), AM generates a corresponding set of inequli-
ties and applies ILP considering known subsumption and disjointness.
3. For solving these inequalities, RMP starts with artificial variables, P 0 is
initially empty, and Q∃ = {RB , Ro1 }, Q∀ = ∅ and Qo = {Io1 } (see Fig.
3). The objective of (PP 1a) uses the dual values from (RMP 1a). For each
at-least restriction a constraint (e.g., ∃R.B rRB − bB ≤ 0) is added to
(PP 1a), which indicates that if rRB = 1 then a variable bB will also be 1.
Constraint (i) ensures that B and o1 cannot exist in same partition element.
Constraint (ii) ensures the semantics of nominals.
4. The values of rRo1 , rIo1 are 1 in (PP 1a), therefore, the variable xRo1 Io1 is
added to (RMP 1b). Since only one b variable (i.e., bo1 ) is 1, the cost of
xRo1 Io1 is 1. P 0 = {{Ro1 , Io1 }} and the value of the objective function is
reduced from 30 in (RMP 1a) to 11 in (RMP 1b).
RMP 1a PP 1a
Min Min
10hRB + 10hRo1 + 10hIo1
bB + bo1 − 10rRB − 10rRo1 − 10rIo1
Subject to: hRB ≥ 1
hRo1 ≥ 1 Subject to:
r RB − b B ≤ 0 bB + bo1 ≤ 1 (i)
hIo1 = 1
rRo1 − bo1 ≤ 0 rIo1 − bo1 = 0 (ii)
Solution: cost = 30, hRB = 1,
hRo1 = 1, hIo1 = 1 Solution: cost = −19, rRB = 0,
Duals: πRB = 10, πRo1 = 10, ωIo1 = 10 rRo1 = 1, rIo1 = 1, bB = 0, bo1 = 1
Fig. 3. Node x: First ILP iteration
Min RMP 1b PP 1b
Min
xRo1 Io1 + 10hRB + 10hRo1 + 10hIo1
bB + bo1 − 10rRB − 10rRo1 + 9rIo1
Subject to: h RB ≥ 1
Subject to:
xRo1 Io1 + hRo1 ≥ 1
r RB − b B ≤ 0 bB + bo1 ≤ 1 (i)
xRo1 Io1 + hIo1 = 1
rRo1 − bo1 ≤ 0 rIo1 − bo1 = 0 (ii)
Solution: cost = 11, xRo1 Io1 = 1,
hRB = 1, hRo1 , hIo1 = 0 Solution: cost = −9, rRB = 1,
Duals: πRB = 10, πRo1 = 10, ωIo1 = −9 rRo1 = 0, rIo1 = 0, bB = 1, bo1 = 0
Fig. 4. Node x: Second ILP iteration
5. As the value of rRB is 1 in (PP 1b), the variable xRB is added to (RMP 1c).
P 0 = {{Ro1 , Io1 }, {RB }} and the cost is further reduced from 11 in (RMP
1b) to 2 in (RMP 1c).
6. All artificial variables in (RMP 1c) are zero which might indicate that we
have reached a feasible solution. The reduced cost of (PP 1c) is not negative
anymore which means that (RMP 1c) cannot be improved further. Therefore,
AM terminates after third ILP iteration and returns the optimal solution
σ(x) = {h{R} , {o1} , 1i, h{R} , {B} , 1i}.
7. The fil -Rule creates two new nodes x1 and x2 with L(x1 ) ← {o1}, L(x2 ) ←
{B}, ]x1 ← 1 and ]x2 ← 1.
8. The e-Rule creates edges hx, x1 i and hx, x2 i with L (hx, x1 i) ← {R, S} and
L (hx, x2 i) ← {R, S} (because R v S ∈ R). It also creates back edges hx1 , xi
and hx2 , xi with L (hx1 , xi) ← {R− , S − } and L (hx2 , xi) ← {R− , S − }.
9. By unfolding B in the label of x2 and by applying the u-Rule we get L(x2 ) =
{B, ∃R.C, ∃R− .D, ∀S − .{o2}}.
10. The inverse-Rule encodes information about existing R− -neighbour x of x2
by adding a tuple hx, {R− , S − }i to B(x2 ).
11. AM uses {∃R.C, ∃R− .D} to start ILP. Due to lack of space we cannot provide
the complete RMP and PP solution process here. Since R v S, the universal
restriction ∀S − . {o2} is ensured by adding the following inequalities to PP:
Min RMP 1c PP 1c
xRo1 Io1 +xRB +10hRB +10hRo1 +10hIo1 Min
bB + bo1 − 1rRB − 10rRo1 + 9rIo1
Subject to:
xRB + hRB ≥ 1 Subject to:
xRo1 Io1 + hRo1 ≥ 1 r RB − b B ≤ 0 bB + bo1 ≤ 1 (i)
xRo1 Io1 + hIo1 = 1 rRo1 − bo1 ≤ 0 rIo1 − bo1 = 0 (ii)
Solution: cost = 2, xRo1 Io1 = 1,
xRB = 1, hRB , hRo1 , hIo1 = 0 Solution:
Duals: πRB = 1, πRo1 = 10, ωIo1 = −9 cost = 0, all variables are 0.
Fig. 5. Node x: Third ILP iteration
rR− − rS − ≤ 0, rS − − bo2 ≤ 0, and for all rRq− we added an equality rRq− −
> > >
rR− ≤ 0. Therefore, whenever rRq− = 1 the values of rR− , rS − , bo2 = 1 .
> > >
12. Since B(x2 ) contains hx, {R− , S − }i, AM adds node x in solution. Therefore,
AM returns the solution σ(x2 ) = {h{R} , {C} , 1i , h{R− , S − } , {D, o2} , 1, {x}i}.
13. The fil -Rule creates only one new node x3 with L(x3 ) ← {C} and ]x3 ← 1,
and updates the label of node x with L(x) ← {D, o2}.
14. The e-Rule creates edges hx2 , x3 i and hx3 , x2 i with L (hx2 , x3 i) ← {R, S}
and L (hx3 , x2 i) ← {R− , S − }.
15. By unfolding C in the label of x3 we get L(x3 ) = {C, ∃R.E}. AM gives so-
lution σ(x3 ) = {h{R} , {E} , 1i}. The fil -Rule creates node x4 with L(x4 ) ←
{E} and ]x4 ← 1. The e-Rule creates edges hx3 , x4 i and hx4 , x3 i with
L (hx3 , x4 i) ← {R, S} and L (hx4 , x3 i) ← {R− , S − }.
16. L(x4 ) = {E, ∀S − . {o1}} and after unfolding E the ∀-Rule adds o1 to L(x3 ).
However, o1 already occurs in L(x1 ) and x1 6= x3 . Therefore, the nommerge -
Rule merges node x3 into node x1 .
17. Since no more rules are applicable, the tableau algorithm terminates.
4 Performance Evaluation
We developed a prototype system called Cicada1 that implements our calcu-
lus as proof of concept. Besides the use of ILP and branch-and-price Cicada
only implements a few standard optimization techniques such as lazy unfold-
ing [2,17], nominal absorption [17], and dependency directed backtracking [1] as
well as a ToDo list architecture [24] to control the application of the expansion
rules. Cicada might not perform well for SHOI ontologies that require other
optimization techniques.
Therefore, we built a set of synthetic test cases to empirically evaluate Cicada.
Figure 6 presents some metrics of benchmark ontologies and evaluation results.
We compared Cicada with major OWL reasoners such as FaCT++ (1.6.5) [24],
HermiT (1.3.8) [21], and Konclude (0.6.2) [23].
1
System and test ontologies: https://users.encs.concordia.ca/~haarslev/Cicada
Ontology Metrics Evaluation Results
Ontology Name
#Axioms #Concepts #Ind Cic FaC Her Kon
EU-Members 67 32 28 4.86 TO TO TO
CA-Provinces 32 14 11 2.85 316.4 TO TO
TestOnt-Cons TestOnt-InCons
Ontology Metrics Evaluation Results Evaluation Results
n
#Axioms #Concepts #Ind Cic FaC Her Kon Cic FaC Her Kon
40 92 43 41 3.39 TO TO TO 4.41 TO TO TO
20 53 23 21 1.21 TO TO TO 3.16 TO TO TO
10 33 13 11 0.91 TO TO TO 2.68 401.7 TO TO
7 27 10 8 0.64 1.26 3.47 3.56 2.32 1.48 3.70 3.71
5 23 8 6 0.41 0.02 0.13 0.24 2.21 0.12 0.46 0.14
Fig. 6. Metrics of Benchmark Ontologies and Evaluation Results with runtime in sec-
onds and a timeout of 1000 seconds (TO=timeout, #=Number of..., Ind=Individuals,
Cic=Cicada, FaC=FaCT++, Her=HermiT, Kon=Konclude)
The first benchmark (see top part of Figure 6) uses two real-world ontologies.
The ontology EU-Members (adapted from [10]) models 28 members of European
Union (EU) whereas CA-Provinces models 10 provinces of Canada. We added
nominals requiring 29 EU members and 11 Canadian provinces respectively. The
results show that only Cicada can identify the inconsistency of EU-Members
within the time limit. Moreover, Cicada is more than two orders of magnitude
faster than FaCT++ in identifying the inconsistency of CA-Provinces.
The second benchmark (see bottom part of Figure 6) consists of small syn-
thetic test ontologies that are using a variable n for representing the number of
nominals. In order to test the effect of increased number of nominals we defined
concept C and A as C v ∃R− .A and A v ∃R.X1 u, ..., u∃R.Xn u ∀R.{o1 , ..., on }.
Nominals o1 , ..., on and concepts X1 , ..., Xn are declared as pairwise disjoint. The
first set consists of consistent ontologies in which we declared C and X1 , ..., Xn−1
as pairwise disjoint. The second set consists of inconsistent ontologies in which
we declared C and X1 , ..., Xn as pairwise disjoint. Only Cicada can process the
ontologies with more than 10 nominals within the time limit.
5 Conclusion
We presented a tableau-based algebraic calculus for handling the numerical re-
strictions imposed by nominals, existential and universal restrictions, and their
interaction with inverse roles. These numerical restrictions are translated into
linear inequalities which are then solved by using algebraic reasoning. The alge-
braic reasoning is based on a branch-and-price technique that either computes an
optimal solution, or detects infeasibility. An empirical evaluation of our calculus
showed that it performs better on ontologies having a large number of nomi-
nals, whereas other reasoners were unable to classify them within a reasonable
amount of time. In future work, we will extend the technique presented here to
SHOIQ.
References
1. Baader, F.: The description logic handbook: Theory, implementation and applica-
tions. Cambridge university press (2003)
2. Baader, F., Hollunder, B., Nebel, B., Profitlich, H.J., Franconi, E.: Am empiri-
cal analysis of optimization techniques for terminological representation systems.
Applied Intelligence 4(2), 109–132 (1994)
3. Barnhart, C., Johnson, E.L., Nemhauser, G.L., Savelsbergh, M.W., Vance, P.H.:
Branch-and-price: Column generation for solving huge integer programs. Opera-
tions research 46(3), 316–329 (1998)
4. Chvatal, V.: Linear programming. Macmillan (1983)
5. CPLEX optimizer, https://www.ibm.com/analytics/cplex-optimizer
6. Cucala, D.T., Cuenca Grau, B., Horrocks, I.: Consequence-based reasoning for
description logics with disjunction, inverse roles, and nominals. In: Proceedings of
the 30th International Workshop on Description Logics (July 2017)
7. Cucala, D.T., Cuenca Grau, B., Horrocks, I.: Consequence-based reasoning for
description logics with disjunction, inverse roles, number restrictions, and nominals.
In: Proceedings of the Twenty-Seventh International Joint Conference on Artificial
Intelligence, IJCAI-18. pp. 1970–1976 (2018)
8. Dantzig, G.B., Wolfe, P.: Decomposition principle for linear programs. Operations
research 8(1), 101–111 (1960)
9. Desrosiers, J., Soumis, F., Desrochers, M.: Routing with time windows by column
generation. Networks 14(4), 545–565 (1984)
10. Faddoul, J., Haarslev, V.: Algebraic tableau reasoning for the description logic
SHOQ. Journal of Applied Logic 8(4), 334–355 (2010)
11. Faddoul, J., Haarslev, V.: Optimizing algebraic tableau reasoning for SHOQ: First
experimental results. In: Proceedings of the 23rd International Workshop on De-
scription Logics (DL’10). pp. 161–171 (2010)
12. Farid, H., Haarslev, V.: Handling nominals and inverse roles using algebraic reason-
ing (2018), extended version of the paper published in Proceedings of the Interna-
tional Workshop on Description Logics (DL’18). https://arxiv.org/abs/1810.00916
13. Farsiniamarj, N., Haarslev, V.: Practical reasoning with qualified number restric-
tions: A hybrid Abox calculus for the description logic SHQ. AI Communications
23(2-3), 205–240 (2010)
14. Haarslev, V., Möller, R.: Racer system description. In: Proceedings of the Interna-
tional Joint Conference on Automated Reasoning. pp. 701–705. Springer (2001)
15. Haarslev, V., Timmann, M., Möller, R.: Combining tableaux and algebraic meth-
ods for reasoning with qualified number restrictions. In: Proceedings of the Inter-
national Workshop on Description Logics (DL’01) (2001)
16. Hladik, J.: A tableau system for the description logic SHIO. In: Proceedings of the
Doctoral Programme of IJCAR. vol. 106. Citeseer (2004)
17. Horrocks, I.: Using an expressive description logic: FaCT or fiction? In: Proceedings
of the 6th International Conference on Principles of Knowledge Representation and
Reasoning (KR’98). vol. 98, pp. 636–645 (1998)
18. Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and
role hierarchies. Journal of logic and computation 9(3), 385–410 (1999)
19. Ohlbach, H., Köhler, J.: Modal logics, description logics and arithmetic reasoning.
Artificial Intelligence 109(1-2), 1–31 (1999)
20. Roosta Pour, L., Haarslev, V.: Algebraic reasoning for SHIQ. In: Proceedings of
the International Workshop on Description Logics (DL’12). pp. 530–540 (2012)
21. Shearer, R., Motik, B., Horrocks, I.: HermiT: A highly-efficient OWL reasoner. In:
Proceedings of the OWL: Experiences and Directions (OWLED). vol. 432, p. 91
(2008)
22. Steigmiller, A., Glimm, B., Liebig, T.: Coupling tableau algorithms for expressive
description logics with completion-based saturation procedures. In: Proceedings of
the 7th International Joint Conference on Automated Reasoning (IJCAR’14). pp.
449–463. Springer (2014)
23. Steigmiller, A., Liebig, T., Glimm, B.: Konclude: system description. Web Seman-
tics: Science, Services and Agents on the World Wide Web 27, 78–85 (2014)
24. Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: System description.
In: Proceedings of the International Joint Conference on Automated Reasoning.
pp. 292–297. Springer (2006)
25. Vlasenko, J., Daryalal, M., Haarslev, V., Jaumard, B.: A saturation-based algebraic
reasoner for ELQ. In: Proceedings of the 5th Workshop on Practical Aspects of
Automated Reasoning (PAAR 2016). pp. 110–124. CEUR (2016)
26. Vlasenko, J., Haarslev, V., Jaumard, B.: Pushing the boundaries of reasoning about
qualified cardinality restrictions. In: Proceedings of the International Symposium
on Frontiers of Combining Systems. pp. 95–112. Springer (2017)
27. Zolfaghar Karahroodi, N., Haarslev, V.: A consequence-based algebraic calculus
for SHOQ. In: Proceedings of the International Workshop on Description Logics
(DL’17) (2017)