=Paper=
{{Paper
|id=Vol-1879/paper21
|storemode=property
|title=A Consequence-based Algebraic Calculus for SHOQ
|pdfUrl=https://ceur-ws.org/Vol-1879/paper21.pdf
|volume=Vol-1879
|authors=Nikoo Zolfaghar Karahroodi,Volker Haarslev
|dblpUrl=https://dblp.org/rec/conf/dlog/KarahroodiH17
}}
==A Consequence-based Algebraic Calculus for SHOQ==
https://ceur-ws.org/Vol-1879/paper21.pdf
A Consequence-based Algebraic Calculus for
SHOQ
Nikoo Zolfaghar Karahroodi and Volker Haarslev
Concordia University, Montréal, Canada
n_zolfa@encs.concordia.ca, haarslev@cse.concordia.ca
Abstract. In this paper, we present a novel consequence-based algo-
rithm to perform subsumption reasoning in SHOQ, which support nomi-
nals and Qualified Cardinality Restrictions (QCRs). Our algorithm maps
numerical restrictions imposed by QCRs or nominals to inequalities and
determines the feasibility of inequality systems by means of Integer Lin-
ear Programming.
1 Introduction and Motivation
Most modern DL reasoners, such as HermiT [8], FaCT++ [13], Pellet [12], and
RacerPro [5], implement highly optimized tableau-based algorithms, or its vari-
ations. The main idea of tableau-based algorithms for classification is to sys-
tematically construct a model of the input ontology plus the negation of each
subsumption candidate. If all constructed models by the procedure turn out to
contain an obvious contradiction (clash), one can conclude that the subsumption
candidate holds.
There is another type of reasoning algorithms, called consequence based algo-
rithms, which instead of building counter-models (like tableau-based algorithms),
directly derive logical consequences of axioms in the ontology using inference
rules. These algorithms never check for subsumptions that are not entailed. Typ-
ically, the number of entailed subsumptions is much smaller than the number of
potential subsumptions between ontology concepts. These algorithms can clas-
sify an ontology in a single pass.
Consequence-based (CB) algorithms were first introduced for the DL EL [1].
These algorithms later were extended to DL ELO [7] and Horn-SHIQ [6] –
DLs that support nominals and functional roles respectively, but not disjunc-
tive reasoning. The framework for consequence based calculi was proposed for
ALCI [11], which support disjunctive reasoning, but not Qualified Cardinality
Restrictions (QCRs). Recently this framework was extended to DL SRIQ that
supports QCRs [2], but their time complexity is dependent to the number of
QCRs and the values occurring in them.
However, to the best of our knowledge, none of the existing CB algorithms
could handle the combination of QCRs and nominals efficiently. As we discuss
in Section 3, it is challenging to extend these algorithms to DLs such as SHOQ
that combines different kinds of numerical restrictions: QCRs and nominals.
On the other hand, most existing DL reasoners try to satisfy imposed nu-
merical constraints by exhausting all possibilities. Merely searching for a model
in such an arithmetically uninformed or blind way is usually very inefficient.
Using arithmetic methods can improve the average case performance of numeric
reasoning. Employing this technique for tableau-based reasoning in SHOQ has
shown to have an impressive practical result [4]. The main drawback of this
approach is producing an exponential number of variables.
In Section 3 we extend the framework introduced in [11] to develop a CB
calculus for SHOQ. Our algorithm employs Integer Linear Programming to
properly handle numerical features of the language, while eliminating its draw-
backs in generating numerous variables, by applying optimization techniques,
specifically column and row generation. Thus, although a practical evaluation
of our calculus is still pending, we believe that it is most likely perform well in
practice on SHOQ ontologies.
2 Preliminaries
Description Logics ALCHOQ and SHOQ are defined w.r.t. non-empty and dis-
joint sets of atomic concepts NC , roles NR and nominals No .
Ontologies are interpreted using Tarski-style semantics. An interpretation
I = (∆I , .I ), where ∆I is a non-empty set of elements called the domain, and .I
is an interpretation function that maps each atomic concept A ∈ NC to a subset
of ∆I , and each role R ∈ NR to a subset of ∆I × ∆I .
A Qualified Cardinality Restriction (QCR), also called qualified number re-
striction, specifies a lower (≥ nR.C) or upper (≤ nR.C) bound on the number
of R-successors belonging to a certain concept C, where R ∈ NR . A domain ele-
ment y ∈ ∆I is said to be an R-successor if there exists a domain element x ∈ ∆I
such that x and y are related trough the role R, hx, yi ∈ RI . The set of all R-
successors for a given role R is defined as Succ(R) = {y ∈ ∆I | hx, yi ∈ RI }. A
qualifying concept A is a concept name that occurs in a QCR of the form ≤ nR.A
or ≥ nR.A to impose a minimum or maximum on the number of R-successors
for a role R ∈ NR .
Nominals are known as named individuals. They are also considered as con-
cepts with exactly one instance that will be interpreted as singleton sets. Nom-
inals enable DLs with the notion of uniqueness and identity. There exist many
concepts in the real world that need to be modeled using nominals such as
“Moon”, “Earth” or “Canada”.
A literal L is a concept of the form C, o, ∃R.C, ∀R.C, ≥ nR.C, ≤ nR.C, for
C ∈ NC , o ∈ No and R ∈ NR . The set of all literals is denoted as NL . Through
the rest of this paper we denote a conjunction and disjunction of literals with
K and M , respectively. Furthermore, we identify them as a set of literals and
use them in standard set operations. The conjunction (disjunction) of literals
may be empty, which is abbreviated as > (⊥). An axiom is an expression of
the form C1 v C2 (general concept inclusion (GCI)), R1 v R2 (role inclusion),
or T rans(R) (role transitivity axiom). A SHOQ ontology O is a finite set of
axioms. dm Fn
A clause is a general concept inclusion of the form i=1 Li v i=m+1 Li
where 0 ≤ m ≤ n and each Li is a literal. A clause is normal if each Li
with 1 ≤ i ≤ m is an atomic concept and a clause is a query if each Li with
m+1 ≤ i ≤ n is an atomic concept. In a clause of the form K v M , the conjunc-
tion K is called the antecedent, and the disjunction M is called the consequence.
An ontology O is normalized if each GCI in O is a normal clause. The ontology
O can be converted to a normalized ontology O0 in linear time such that O0 is
a conservative extension of O. This conversion is known as structural transfor-
mation (see, e.g., [6,8]), so we eliminate the details due to space restrictions. A
normalized SHOQ ontology can be rewritten to a normal ALCHOQ ontology
by eliminating all role transitivity axioms [10]. Given a set of literals L, a clause
K v M is over L if K ∪ M ⊆ L. A clause K 0 v M 0 is a strengthening of a clause
K v M if K 0 ⊆ K and M 0 ⊂ M . We use K v M ∈∗ C to show that a set of
clauses C contains at least one strengthening of K v M .
Due to the presence of nominals, assertions can be transformed to termino-
logical knowledge (TBox axioms). So we only consider terminological reasoning
in this research. In SHOQ the interaction of transitive roles with number re-
strictions would cause undecidability. To avoid this interaction, SHOQ allows
number restrictions only with simple roles which are neither transitive nor have
transitive sub-roles.
3 A consequence-based calculus for SHOQ
In this section, we explain our consequence-based algorithm for classifying a
normalized ALCHOQ ontology O having a finite set of queries Q to determine
whether O |= q holds for each query q = K v M ∈ Q. Since the goal of the
algorithm is to obtain the ontology classification, we only consider queries of
the form C1 v C2 where C1 and C2 are atomic concepts from O. A formal
description of our algorithm is presented in Section 3.2.
3.1 Intuition
This section demonstrate our algorithm at a high level by applying it to the
ontology O and the query q as specified in Example 1 to prove that O |= q.
Example 1. Let O be an ontology containing axioms (1) – (9), and q = A v D.
One can readily verify that O |= q due to cardinality restrictions imposed on the
concepts A, C by merging nominals o1 , o2 and o3 .
A v ∃R.o1 (1) A v ∃R.o3 t D (3) o1 v C (5) o1 v ≥ 2S.B (8)
A v ∃R.o2 (2) A v ≤ 1R.C (4) o2 v C (6) B v o1 t o2 t o3 (9)
o3 v C (7)
Our consequence-based algorithm constructs a graph whose vertices are called
nodes. Each node describes a set of elements in the model I, which is an arbi-
trary model. The edges between nodes represent role successor relations be-
tween the corresponding elements. Each node v is associated with an atomic
concept core(v). Intuitively, core(v) holds for every element of I that cor-
responds to v. Moreover, each node v is labeled with a set of clauses L(v).
Each clause K v M ∈ L(v) is related to core(v) and should be interpreted as
core(v) u K v M .
Figure 1 illustrates the constructed graph for Example 1, where each node
is shown as a circle. The core concept of each node v is shown as the subscript
of v inside the circle, and the label of each node, L(v), is shown either below
or above the circle. The numbers next to the clauses in L(v) correspond to the
order of inference rule applications.
The inference process starts by initializing the algorithm according to the
target query. Since in this example the query is q = A v D, we introduce a node
vA where core(vA ) = A, and add clause (10) to L(vA ). Intuitively, this clause
states that there has to be at least one element in the model I that satisfies A.
Since nominals always exist, we also need to create one node vo , for representing
each nominal o occurring in O. Therefore nodes voi for 1 ≤ i ≤ 3 are created to
represent existing nominals and are initialized by clauses (11) – (13).
Afterwards, the subs rule (see Table 1) derives clauses (14) – (20). Since
only A is assumed to hold in vA , the algorithm derives only a linear number of
clauses. This rule is analogous to the Rv rule in the original completion rules
for EL [1] and is adapted from [11].
Clause (14) and (15) state that vA must have R-successors o1 I and o2 I
respectively. Clause (16) says that all the corresponding elements to vA must
have an R-successor o3 I or should satisfy D. On the other hand, clause (17)
indicates that all the corresponding elements to vA must have at most one R-
successor in which C holds.
The Nom rule finds a solution ξ that satisfies all these restrictions by means
of an Integer Linear Programming (ILP) Component. This component is called
whenever a QCR is added to the label of a node. Before feeding numerical restric-
tions to the ILP component, every number restriction should be encoded into
an inequality. The encoding procedure will be discussed thoroughly in Section
4. The ILP component may also receive other information such as the subsump-
tion relations in vo1 and vo2 in order to find a more constrained solution that is
less likely to cause a contradiction later due to added entailments. The atomic
concepts that participate in a disjunction with QCRs would not be reflected in
inequalities, e.g., concept D in clause (16).
If the inequality system is feasible, the ILP component returns a possible
solution which satisfies all numerical restrictions. The returned solution is a set
of tuples each containing a partition element and its cardinality (see Section
4). In Example 1, the ILP component returns ξ(vA ) = {h{o1 , o2 , C}, 1i}. Which
means that, for satisfying the submitted constraints (14)-(17), there should exist
one element in the domain in which o1 , o2 and C hold. Due to the presence of
nominals in the returned solution the Nom rule is applicable, which essentially
checks if a nominal o always would appear in a partition element p together
with a concept C ∈ p (or another nominal o2 ∈ p). Accordingly, the Nom rule is
applicable for nominals o1 and o2 and derives clauses (21) and (22).
The Nom rule does not apply to nominal o3 , because clause (16) represents a
possibility and if D is true in (16) then o3 does not have to exist in a partition
element with o1 and o2 . However, the consequences of assuming o3 to be equal to
o1 and o2 still have to be checked. To reflect this possible equality in the graph,
the Sigma rule adds clauses (26) – (29) to the graph. In general, the select
function chooses a concept X of each partition element p as its representative.
The concept X would be the core of a node v (core(v)= X). A clause D v D
is added to the label of a node vX for every other concept D that holds in p,
which reflects the possibility of holding D for elements corresponding to vX .
Clauses (26) and (21) state that o1 , o2 and o3 are possibly merged, so, based
on Clause (9) the cardinality of B would to be less than or equal to one. Clause
(30) requires at least two elements in B I . One can verify that these constraints
are infeasible altogether. The ILP component discovers this infeasibility and
returns a set of clash culprits (Definition 7) that cause the contradiction. A
clash culprit is the minimum set of literals such that their conjunction causes
an infeasibility.
In this example, clauses o1 v o2 , o1 v o3 , o1 v ≥ 2R.B and B v o1 t o2 t o3
would be returned as a clash culprit altogether. But o1 v o3 is the only possible
clause (shown by clause (26) and (28)) that participates in the contradiction.
One can see that all (i.e. in our example, the only one) possible clauses that
cause the clash exist in the label of the same node (L(o1 )). Thus applying the
Bottom rule adds clause (31) – (34) to the graph.
Clause (31) states that nominals o1 , o3 can not hold (be merged) together,
which makes the inequality system containing clauses (14) - (17) infeasible. There
is only one possible clause in the returned clash culprits which is A v ∃R.o1 and
it belongs to L(vA ), so, the Bottom rule produces clause (35).
Later, the inequality system corresponding to clauses (30) and (21) becomes
feasible. Based on the solution returned by ILP, the Sigma rule requires two nodes
corresponding to o2 and o3 . But then, there is no need to introduce fresh nodes
with cores o2 and o3 because our algorithm is designed to reuse the existing
nodes vo2 and vo3 . Consequently, we introduce edges (36) and (37) using the
Sigma rule.
Our reuse strategy is comparable to blocking techniques in tableau-based
algorithms but is much more efficient in eliminating redundant computations.
First, our algorithm never needs more than a linear number of nodes to the
number of concepts occurring in ontology O, whereas tableau-based algorithms
can construct trees of double exponential size. Second, the clauses in the label
of each node are not localized to a specific element in I, and so our algorithm
draws the inferences for a particular core only once.
Eventually, we use the Sigma rule to add clause (38), (39), and (40). At this
point no further inference rule is applicable. Since all clauses are “relative” to the
initialization : > v o3 (13)
Subs[7, 13] : >vC (20) initialization : >vA (10)
Sigma[14 − 17] : o1 v o1 (28) Subs[1, 10] : > v ∃R.o1 (14)
Sigma[14 − 17] : o2 v o2 (29) Subs[2, 10] : > v ∃R.o2 (15)
Bottom[9, 21, 26, 30] : o1 v ⊥ (33) Subs[3, 10] : > v ∃R.o3 t D (16)
Bottom[9, 21, 26, 30] : o2 v ⊥ (34) Subs[4, 10] : > v ≤ 1R.C (17)
Simga[9, 21, 26, 30] : BvB (40) Bottom[14, 15, 16, 17, 31] : > v D (35)
Sigma[14 − 17] : R (25)
vo3 vA
Simga[9, 21, 26, 30] : S
Sigma[14 − 17] : R (24)
3)
(37)
(2
R
]:
17
−
[14
gma
Si
Simga[9, 21, 26, 30] : S
(36)
vo1 vo2
initialization : > v o1 (11) initialization : > v o2 (12)
Subs[5, 11] : >vC (18) Subs[6, 12] : >vC (19)
N om[14 − 17] : > v o2 (21) N om[14 − 17] : > v o1 (22)
Sigma[14 − 17] : o3 v o3 (26) Sigma[14 − 17] : o3 v o3 (27)
Subs[11, 8] : > v ≥ 2S.B (30) Bottom[9, 21, 26, 30] : o3 v ⊥ (32)
Bottom[9, 21, 26, 30] : o3 v ⊥ (31) Simga[9, 21, 26, 30] : BvB (39)
Simga[9, 21, 26, 30] : BvB (38)
Fig. 1. Example inferences of the consequence-based algorithm
core of the corresponding node, clause (35) corresponds to A v D, so we have
proved O |= A v D. In fact, due to (35), we know that O |= K v M for each
query K v M such that A v D is a strengthening of K v M .
We are aware that an unrestricted application of the Subs rule can overwhelm
the whole graph with produced clauses. So, our next step will be to extend our
algorithm to employ an ordered resolution variant addressing this problem [9].
3.2 Formalization
In the following, we provide a formal description of our consequence-based rea-
soning algorithm by introducing a set of inference rules shown in Table 1, the
Subs rule is adapted from [11] but the rest of rules are original. Before for-
mally defining our algorithm, we present some notions which are used later in
formalizing our inference rules.
Definition 1 (Completion Graph). A Completion Graph G = (V, E, L) is
composed of a set of nodes. Each node v is labeled by an atomic concept C
which is called core(v) and a set of clauses L(v). Each edge hu, vi ∈ E is labeled
by the set L(hu, vi) ⊆ R.
In addition, G is over a set of literals L ⊆ NL if L contains all literals in G.
Through the rest of this paper we fix L to contain the set of literals occurring
in O ∪ Q since O and Q are finite, set L is finite as well. Assuming v to be an
arbitrary node in G and q = K v M to be an arbitrary query; then v covers q
if core(v) ⊆ K.
Definition 2 (Clause System). A clause system for a completion graph G
is a function L that assigns a set of clauses L(v) to each node v ∈ V. It is
possible to decide query entailment based on L: A query q = K v M is entailed,
O |= K v M , if and only if K v M ∈ L(v), for each node v covering q and
initialized so that K v L ∈∗ L(v) holds for each literal L ∈ K.
Theorem 1 states that all clauses derived by our calculus are indeed conclu-
sions of the input ontology. The completeness of our algorithm is ensured by
Theorem 2.
Definition 3 (Soundness). A completion graph G is sound for O, if for ev-
ery edge R ∈ L(hv, ui), there exist arbitrary elements α, β ∈ ∆ such that α ∈
(core(v))I , β ∈ (core(u))I and O |= hα, βi ∈ RI . A clause system L is sound
for O if O |= core(v) u K v M holds for each node v ∈ V and each clause
K v M ∈ L(v).
Theorem 1 (Soundness). Let G 1 be a completion graph and let L1 be a clause
system for G1 . The completion graph G2 and the clause system L2 are obtained
by applying an inference rule from Table 1 to G1 and L1 . If G1 and L1 are sound
for O, then both G2 and L2 are sound for O.
Theorem 2 (Completeness). Let G be a completion graph and let L be a
clause system for G such that no inference rule from Table 1 is applicable to G
and L. Then K v M ∈∗ L(v) hold for each query q = K v M and each node
v ∈ V if O |= K v M and K v L ∈∗ L(v) for each literal L ∈ K.
Definition 4 (Known/Possible QCRs). The set Qk (v) contains QCRs which
are known to hold in a node v for which > v ≤ nR.C or > v ≥ nR.C has been
derived in node v. Set Qp (v) contains QCRs that can possibly hold in a node v.
These are those QCRs for which K v ≤ nR.L t M or K v ≥ nR.L t M has
been derived in node v for some K 6≡ > or M 6≡ ⊥. The set Qp (v) is formally
defined as Qp (v) = {./ nR.C | K v ./ nR.C t M ∈ L(v), K 6≡ > or M 6≡ ⊥}.
Definition 5 (Possible Clause). The set C p (v) contains possible clauses that
are considered to hold in a node v. A clause K v M ∈ L(v) is a possible clause,
if either K ≡ > or M ≡ ⊥, otherwise, it would be a known clause. The set of
known clauses in the label of a node v is denoted as C k (v).
Definition 6 (select function). The select function chooses one qualifying
concept C ∈ p as the core, where C is either a qualifying concept in a known at-
least restriction or a nominal, and p a partition element. If p contains a nominal
o, then the select function always selects the nominal o as the representative
for p. But if p contains more that one nominal then all of them are selected, one
after the other. The consequences of the rule are applied to all these nominals.
The method select is called a function because it returns a unique representative
for all partition elements containing the same set of concepts.
Definition 7 (Clash Culprits (CC(v))). A Clash Culprit set (CC(v) =
{CC1 (v), ..., CCn (v)}) is returned by the ILP component if an inequality system
is infeasible. A CCi , 1 ≤ i ≤ n consists of the minimum number of clauses such
that the inequality system containing the corresponding inequalities is infeasible.
Note that there may be more than one clash culprit for the same set of in-
equalities. For example assume we are trying to check the satisfiability of the
QCRs: ≥ 2R.C, ≥ 3R.C and ≤ 1R.C. One can recognize two clash culprits in
CC(v) that are involved in the clash, CC1 = {≥ 2R.C, ≤ 1R.C} and CC2 = {≥
3R.C, ≤ 1R.C}. Considering each set of clash culprits may lead to a subsump-
tion. Accordingly, we need to apply the Bottom rule for each CCi .
If all the clauses in a clash culprit are known information, we call it a strict
unsatisfiablity, which can not be avoided by choosing an other possibility. The
Bottom rule only considers possible clauses in a clash culprit set because known
clauses can never be violated. Therefore, if all the clash culprits are known then
it means that there is an unsatisfiability in the ontology. All clauses of a clash
culprit set may not necessarily occur in the label of one particular node. In this
case, no clauses can be derived based on the current knowledge.
4 Integer Linear Programming Component
We implement the ILP services in a separate module called the ILP component.
The task of the ILP Component can be divided into three parts: producing
variables, encoding numerical restrictions into inequalities and checking the sat-
isfiability of derived inequalities.
The ILP component would be called for checking the satisfiablity of QCRs
in the label of a node v. Each time, all QCR occurring in the label of v and all
clauses in C k (vC ), C k (vo ) and C p (vo ) are fed to ILP component, where C ∈ Qv
and o ∈ No (v).
4.1 Decomposition Set
A decomposition set DS needs to include role successors of all related roles for
a node v, which is defined as R(v) = {R | ./ n R.A occurs in L(v)}. If a role R
appears in a partition element p, R ∈ p, it means that all the elements of pI
should be R successors. If a role does not appear in p, the elements of pI are
assumed to be R0 successors where R0 is the complement of R.
One needs to include qualifying concepts in the decomposition set to cap-
ture the semantics of QCRs and also to handle their possible interaction with
nominals. It allows to distinguish cases where role successors have different qual-
ifications. When a partition element p includes a concept name A, it means that
all the elements of pI are elements of AI . Otherwise, they are assumed to be el-
ements of (¬A)I . The set of qualifying concepts of R related to node v is defined
as Qv (R) = {A | ./ nR.A occurs in L(v)}. Accordingly,
S the set of all qualifying
concepts related to a node v is defined as Qv = R∈R(v) Qv (R).
Having nominals as part of our decomposition set allows reflecting their se-
mantics in inequalities. Besides, the interpretation of each nominal o ∈ No may
interact with successors of a role R ∈ NR if oI ⊆ Succ(R). Additionally, The
same nominal can interact with role successors of another role S. In this case,
although R and S may not be related to each other according to the role hierar-
chy, their role successors may interact due to their interaction with the common
nominal. If a nominal o ∈ No is part of a partition element p, then it means that
all the elements of pI have to be in oI . The set of related nominals for a node v,
No (v) ⊆ No , is defined as No (v) = {o | o occurs in L(vC ) such that C ∈ Qv }. If
a nominal o is not part of p then its negation ¬o is added to p by default. The
restrictions imposed by nominals can not be handled node-locally. That is why
nominals participate in the decomposition set of all related nodes.
Definition 8 (Decomposition Set). A decomposition set DS(v) is defined for
each node v, as DS(v) = R(v) ∪ Qv ∪ No (v).
Definition 9 (Partition). A partition P is the power set of DS(v) ∪ N¬o ,
where N¬o is the set of the negation of all nominals occurring in O. Each p ∈ P
is associated with a variable σ p , which is equal to the cardinality of pI .
4.2 Deriving Inequalities
The partition elements p ∈ P are defined using the atomic decomposition tech-
nique, so they are semantically pairwise disjoint. Since the cardinality function
of disjoint sets is additive, one can encode a cardinality restriction into an in-
equality using the sum of cardinalities, shown by δ sq , such that for each sq ⊆ DS
we have δsq = Σsq⊆p σp for all p ∈ P. Roughly speaking, δsq is the sum of car-
dinalities of all partition elements containing sq. For example if DS = {R, C, o}
then δR = σRCo + σRC + σRo + σR and δRC = σRCo + σRC . Hence, a cardinality
bound imposed by QCRs or nominals on a subset of domain elements distributed
over the elements in P can be encoded into inequalities as follows.
QCRs of the form ≤ nR.C or ≥ mS.D are mapped to inequalities δRC ≤ n
or δSD ≥ m respectively. Based on nominal semantics, the sum of cardinalities
of all partition elements containing a particular nominal should be equal to 1.
We encode this cardinality bound by adding two inequalities of the form δo ≤ 1
and δo ≥ 1, for each nominal o ∈ No .
Providing more information to the ILP component reduces the risk that
a solution is returned which will fail later due to newly derived entailments.
Table 1. Inference Rules for reasoning in ALCHOQ
dn
If i=1 Ai v M ∈ O,
Subs Ki v Mi t Ai ∈ L(v)
and n Ki v M t n
d F
Mi ∈/ ∗ L(v)
di=1 Fi=1
then n
add i=1 Ki v M t n i=1 Mi to L(v)
If there exists p occurring in ξ(v) such that R ∈ p and
no edge hv, ui ∈ E exists
such that R ∈ Lhv, ui and L v L ∈∗ L(u) for each L ∈ p
then let u = select(p)
Sigma
if u does not exist,
then create node u and L(u) = {> v L | L ∈ core(u)};
if hv, ui does not exist,
then create edge hv, ui; and add R to L(hv, ui); and
for each L ∈ p\core(u) such that L v L ∈/ ∗ L(u), add L v L to L(u).
If there exists p occurring in ξ(v) such that a nominal o ∈ p ,
and a concept/nominal D ∈ p and,
Nom
L(v) ∪ {o u D v ⊥} causes a strict unsatisfiability and,
>vD∈ / ∗ L(o),
then add > v D to L(o).
If there exists a node u such that core(u) u Ki v Mi t Li ∈ CCj (v) for 0 ≤ i ≤ n,
CCj (v) ∈ CC(v),
Bottom
S
where either Li ∈ Qp (v) or core(u) u Ki v Mi t Li ∈ o∈No C p (o) and,
dn Fn
i=0dKi v i=0FMi ∈
/ ∗ L(u),
then add n i=0 Ki v
n
i=0 Mi to L(u).
Feeding subsumptions and disjointness to the ILP component allows the so-called
infeasible operator to set the cardinality of some partition elements to zero. For
this purpose, we define a binary variable bC ∈ {0, 1}, C ∈ DS, associated with
each member of a decomposition set in order to apply conditional constraints on
the presence of a role, concept or nominal in a partition element. Assuming that
b⊥ ≤ 0, we use binary variables and inequalities to disable infeasible partition
elements, using the mappings presented below.
SubsumptiondRelation Assuming that
n Fmin a clause of the form K v M ,
where K denotes i=1 Li and M denotes j=1 Lj , all the literals are atomic
concepts or nominalsP and Li ∈ DS. Then the PmILP component maps clause K v
n
M to the inequality i=1 bLi − (n − 1) ≤ j=1 bLj . For example translating a
subsumption relation A v B produces bA ≤ bB , which ensures that if a partition
element contains the atomic concept A, it should contain A’s subsumer B. In
other words the cardinality of a partition element which contains A but not B
has to be equal to zero.
This mapping can also be used for encoding axioms of the form A v o1 t o2
where o1 and o2 are two nominals. The obtained inequality, bA ≤ bo1 + bo2 ,
guarantees that if a partition element contains the atomic concept A then it
has to contain either o1 or o2 , i.e., the cardinality of a partition element that
contains A but neither o1 nor o2 , should be equal to zero.
Role Subsumption Every role subsumption relation of the form R v S can
be encoded to the inequality bR ≤ bS . This inequality ensures that if a partition
element contains a subrole R, it must contain all of R’s superroles, otherwise the
cardinality of such a partition element should be equal to zero.
Universal Restriction A universal restriction of the form ∀R.A can be
encoded to the inequality bR ≤ bA . The semantics of universal restriction implies
that all R successors are instance of A. The generated inequality satisfies this
semantics by implying that if a partition element contains the role R it should
also contain the concept A.
4.3 Returning Solution or Clash Culprits
Lemma 1. If the submitted inequality system to the ILP component is feasible,
it will return a solution that satisfies all the constraints. The returned arithmetic
solution assigns a positive integer n to σp , which denotes the cardinality of the
corresponding partition element. The ILP component would iterative through all
possible solutions that exist for solving an equality system [3].
Definition 10 (Arithmetic Solution). An arithmetic solution ξ(v) is a set of
tuples hp, σp i produced by the ILP component for solving a particular inequality
system related to a node v, where p is a partition element and σ p ∈ N, σp ≥ 1 is
the cardinality of p.
If the inequality system is infeasible, then the ILP component returns the
smallest set of clauses, called clash culprit set (Definition 7), such that the in-
equality system containing their corresponding inequalities is infeasible. There
may be more than one minimum clash culprit set for each inequality system.
5 Summary and Conclusion
This paper presented an algebraic consequence-based reasoning algorithm for
SHOQ. To the best of our knowledge, this is the first extension of consequence-
based algorithms for the expressive description logic SHOQ. During the reason-
ing process, only one node is created for representing elements associated with
each concept. Using a representative node for each concept not only helps in re-
ducing the size of the generated framework but also allows for re-using elements.
In contrast to tableau-based reasoners, our calculus naturally handles cyclic de-
scriptions without the need for any blocking strategies to ensure termination.
Unlike most reasoning algorithms for SHOQ, the algebraic consequence-
based method allows arithmetically informed reasoning about the numerical re-
strictions on domain elements by mapping numerical restrictions to inequali-
ties and handling obtained inequality systems using integer linear programming
methods. The consequence-based SHOQ reasoning is based on the atomic de-
composition technique which is applied to the proper decomposition set allowing
the calculus to handle the various interactions between nominals, role successors
and their qualifications. The inference rules are designed in a way to derive all
consequences of presented axioms while benefiting from lazy unfolding to avoid
overwhelming the framework with unnecessary axioms. The inference rules are
inspired by resolution to resolve complement literals.
References
1. F. Baader, S. Brandt, and C. Lutz. Pushing the EL envelope. In Proceedings of
the 19th International Joint Conference on Artificial Intelligence, pages 364–369,
San Francisco, CA, USA, 2005. Morgan Kaufmann Publishers Inc.
2. A. Bate, B. Motik, B. C. Grau, F. Simancik, and I. Horrocks. Extending
consequence-based reasoning to SRIQ. In C. Baral, J. P. Delgrande, and
F. Wolter, editors, KR, pages 187–196. AAAI Press, 2016.
3. J. Faddoul. Reasoning Algebraically with Description Logics. PhD thesis, Concordia
University, Montreal, Quebec, Canada, September 2011.
4. J. Faddoul and V. Haarslev. Algebraic Tableau Reasoning for the Description Logic
SHOQ. Journal of Applied Logic, Special Issue on Hybrid Logics, 8(4):334–355,
December 2010.
5. V. Haarslev and R. Möller. Racer system description. In Proc. of the Int. Joint
Conf. on Automated Reasoning (IJCAR 2001), volume 2083 of Lecture Notes in
Artificial Intelligence, pages 701–705. Springer, 2001.
6. Y. Kazakov. Consequence-driven reasoning for Horn-SHIQ ontologies. In
C. Boutilier, editor, Proceedings of the 22nd International Workshop on Descrip-
tion Logics (DL 2009), Oxford, UK, July 27-30, 2009, pages 2040–2045, 2009.
7. Y. Kazakov, M. Krötzsch, and F. Simančík. Practical reasoning with nominals in
the EL family of description logics. In G. Brewka, T. Eiter, and S. A. McIlraith, ed-
itors, Proceedings of the 13th International Conference on Principles of Knowledge
Representation and Reasoning (KR’12), pages 264–274. AAAI Press, 2012.
8. B. Motik, R. Shearer, and I. Horrocks. Hypertableau reasoning for description
logics. Journal of Artificial Intelligence Research, 36:165–228, 2009.
9. J. A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning (in
2 volumes). Elsevier and MIT Press, 2001.
10. F. Simančík. Consequence-Based Reasoning for Ontology Classification. PhD the-
sis, University of Oxford, 2013.
11. F. Simančík, B. Motik, and I. Horrocks. Consequence-based and fixed-parameter
tractable reasoning in description logics. Artificial Intelligence, 209:29–77, 2014.
12. E. Sirin, B. Parsia, B. Grau, A. Kalyanpur, and Y. Katz. Pellet: A practical
OWL-DL reasoner. Journal of Web Semantics, 5(2):51–53, 2007.
13. D. Tsarkov and I. Horrocks. Fact++ description logic reasoner: System description.
In Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2006), volume
4130 of Lecture Notes in Artificial Intelligence, pages 292–297. Springer, 2006.