=Paper=
{{Paper
|id=Vol-1193/paper_18
|storemode=property
|title=A MILP-based Decision Procedure for the (Fuzzy) Description Logic ALCB
|pdfUrl=https://ceur-ws.org/Vol-1193/paper_18.pdf
|volume=Vol-1193
|dblpUrl=https://dblp.org/rec/conf/dlog/BobilloS14
}}
==A MILP-based Decision Procedure for the (Fuzzy) Description Logic ALCB==
https://ceur-ws.org/Vol-1193/paper_18.pdf
A MILP-based decision procedure for the
(Fuzzy) Description Logic ALCB
Fernando Bobillo1 and Umberto Straccia2
1
Dpt. of Computer Science & Systems Engineering, University of Zaragoza, Spain
2
Istituto di Scienza e Tecnologie dell’Informazione (ISTI - CNR), Pisa, Italy
Email: fbobillo@unizar.es, straccia@isti.cnr.it
Abstract. To overcome the inability of Description Logics (DLs) to
represent vague or imprecise information, several fuzzy extensions have
been proposed in the literature. In this context, an important family of
reasoning algorithms for fuzzy DLs is based on a combination of tableau
algorithms and Operational Research (OR) problems, specifically using
Mixed Integer Linear Programming (MILP). In this paper, we present a
MILP-based tableau procedure that allows to reason within fuzzy ALCB,
i.e., ALC with individual value restrictions. Interestingly, unlike classical
tableau procedures, our tableau algorithm is deterministic, in the sense
that it defers the inherent non-determinism in ALCB to a MILP solver.
1 Introduction
Description Logics (DLs for short) [2] are a family of logics for representing
structured knowledge. In the last two decades, DLs have gained even more pop-
ularity due to their application in the context of the Semantic Web [3]. Indeed,
the current standard language for specifying ontologies is the Web Ontology
Language (OWL 2) [18], which is based on the DL SROIQ(D) [23].
Fuzzy DLs have been proposed as an extension to classical DLs with the aim
of dealing with fuzzy/vague/imprecise concepts by including elements of fuzzy
logic [35]. In fuzzy DLs, the axioms may not be bivalent, but instead can be
satisfied with a certain degree of truth (typically, a truth value in [0, 1]). Since
the first work of J. Yen in 1991 [34], an important number of works can be found
in the literature (good surveys on fuzzy DLs can be found on [25,33]).
Several families of algorithms to reason with fuzzy DLs have been proposed
in the literature. The most important ones are tableau algorithms [15,28,29,30],
tableau algorithms combined with Operational Research (OR) problems [8,17],
automata-based algorithms [14,13], reduction to classical DLs [4,5,6,10,12], and
reduction to fuzzy logics [16,19,22].
Some of the existing algorithms already support nominals. A tableau al-
gorithm for Zadeh SHOIQ [28] and an algorithm to check subsumption in
Gödel EL++ [26] are both able to deal with nominals. There are also reduc-
tions to classical DLs for fuzzy SROIQ(D) under Zadeh [4], finite Gödel [5],
finite Lukasiewicz [10], and any finite t-norm [6]; but also for SHOI for every
t-norm not starting with the Lukasiewicz t-norm [12].
However, to the best of our knowledge, none of the existing OR-based tableau
algorithms is able to support nominals so far. This family of algorithms is inter-
esting for several reasons: (i) it is very suitable to manage fuzzy datatypes [31]
or fuzzy concepts without a counterpart in classical DLs, such as fuzzy modified
concepts [31] or aggregated concepts [11]; (ii) it makes it possible to reason with
other t-norms different than Gödel [8]; and (iii) the arguably most popular fuzzy
ontology reasoner fuzzyDL implements one of these algorithms [7].
The objective of this paper is to start filling this gap by proposing a novel
decision procedure for a fuzzy DL with individual value restrictions, namely
ALCB. ALCB is the basic DL language ALC [31] extended with individual value
restrictions. Under the restriction that the TBox is acyclic, our algorithm applies
for Lukasiewicz, Zadeh fuzzy DLs, and for classical DLs.
The rest of this paper is organised as follows. Section 2 includes some prelimi-
nary notions. Section 3 presents our reasoning algorithm and Section 4 a running
example. Finally, Section 5 sets out some conclusions and ideas for future work.
2 Fuzzy DLs Basics
In this section we overview some basic definitions on mathematical fuzzy logic
and the fuzzy DL ALCB (see [25,33] for a more in depth presentation).
Mathematical Fuzzy Logic. In Mathematical Fuzzy Logic [21], the usual conven-
tion prescribing that a statement is either true or false is changed and is a matter
of degree measured on an ordered scale that is no longer {0, 1}, but e.g., [0, 1].
This degree is called degree of truth of the logical statement φ in the interpreta-
tion I. For us, fuzzy statements have the form hφ, αi, where α ∈ (0, 1] and φ is a
statement, encoding that the degree of truth of φ is greater than or equal to α.
Fuzzy logics provide compositional calculi of degrees of truth. The conjunc-
tion, disjunction, complement and implication operations are performed in the
fuzzy case by a t-norm function ⊗, a t-conorm function ⊕, a negation function
and an implication function ⇒, respectively (see [21] for definitions and proper-
ties of these functions). A quadruple composed by a t-norm, a t-conorm, an im-
plication function and a negation function determines a fuzzy logic. One usually
distinguishes three fuzzy logics, namely Lukasiewicz, Gödel, and Product [21],
due to the fact that any continuous t-norm can be obtained as a combination
of Lukasiewicz, Gödel, and Product t-norm [27]. It is also usual to consider also
Zadeh logic. The combination functions of these logics can be found in Table 1.
It is easy to see that Zadeh fuzzy logic can be expressed using Lukasiewicz
fuzzy logic, as min(α, β) = α ⊗L (α ⇒L β), max(α, β) = 1 − min(1 − α, 1 − β),
and α ⇒KD β = max(1 − α, β). This latter implication is called Kleene-Dienes
implication. The name of Zadeh fuzzy logic is used following the tradition in the
setting of fuzzy DLs, even if the name may lead to confusion because the logic
does not usually include Rescher implication, sometimes called Zadeh implication
as well. This implication is defined as α ⇒ β = 1 if α ≤ β; 0 otherwise.
Table 1. Truth combination functions of various fuzzy logics.
Lukasiewicz logic Gödel logic Product logic Zadeh logic
α ⊗ β max(α + β − 1, 0) min(α, β) α·β min(α, β)
α⊕β min(α + β, 1) ( max(α, β) α+β−α·β max(α, β)
1 if α ≤ β
α ⇒ β min(1 − α + β, 1) min(1, β/α) max(1 − α, β)
β otherwise
( (
1 if α = 0 1 if α = 0
α 1−α 1−α
0 otherwise 0 otherwise
The Fuzzy DL ALCB. This logic is obtained by extending fuzzy ALC with
individual value restrictions (indicated with the letter B). It is a sublogic of the
fuzzy DL presented at [32]. Let A be a set of concept names (also called atomic
concepts), R be a set of role names, and I be a set of individual names. Each role
R ∈ R is also called an object property. The set of concepts (denoted C, D) is
built from concept names A ∈ A using connectives and quantification constructs
over roles R and individuals a ∈ I, according to the following syntactic rule:
C, D → A | (atomic concept)
> | (universal concept)
⊥ | (bottom concept)
¬C | (concept negation)
C u D | (concept conjunction)
C t D | (concept disjunction)
∀R.C | (universal restriction)
∃R.C | (existential restriction)
∃R.{a} | (individual value restriction) .
Now we will define the axioms that can be expressed in a fuzzy ontology. A
fuzzy knowledge base or fuzzy ontology is a tuple K = hA, T i, where A is an
ABox with assertional axioms and T is a TBox with terminological axioms. In
the axioms, we will use α ∈ (0, 1] to denote a truth value. If α is omitted, α = 1
is assumed.
An ABox A (Assertional Box) is a finite set of concept assertions or role
assertions. A concept assertion ha :C, αi states that a is an instance of concept
C to degree at least α. Furthermore, a role assertion h(a1 , a2 ) :R, αi indicates
that (a1 , a2 ) is an instance of role R to degree at least α.
A TBox T (Terminological Box) is a finite set of General Concept Inclusion
(GCI) axioms of the form hC v D, αi, indicating that C is a sub-concept of D
to degree at least α. C is called the head and D is the body of the axiom. C = D
can be used as a shorthand for both hC v D, 1i and hD v C, 1i. For a concept
name A, we say that a definitional axiom is of the form A = C, while a primitive
inclusion axiom is of the form A v C. Furthermore, we say that A1 directly uses
A2 w.r.t. T if A1 is the head of some axiom and A2 occurs in its body. Let
uses be the transitive closure of the relation directly uses. T is acyclic if it has
primitive or definitional axioms only, a concept name A is the head of at most
one definitional axiom in T , there is no concept name A in the head of both a
definitional and primitive inclusion axiom, and there is no concept name A such
that A uses A.
Example 1. We have built a fuzzy wine ontology 3 according to the FuzzyOWL 2
proposal [9]. Ontologies often use individual value restrictions to state geographi-
cal origins. For instance, the fuzzy wine ontology contains the following definition
of Tuscan wines: TuscanWine = Wine u ∃locatedIn.{TuscanyRegion}.
Now, let us formally specify the semantics. Let us fix a fuzzy logic. In classical
DLs, an interpretation I maps e.g., a concept C into a set of individuals C I ⊆
∆I , i.e., I maps C into a function C I : ∆I → {0, 1} (either an individual
belongs to the extension of C or does not belong to it). However, in fuzzy DLs,
I maps C into a function C I : ∆I → [0, 1] and, thus, an individual belongs to
the extension of C to some degree in [0, 1], i.e., C I is a fuzzy set. Specifically, a
fuzzy interpretation is a pair I = (∆I , ·I ) consisting of a non-empty (crisp) set
∆I (the domain) and of a fuzzy interpretation function ·I that assigns:
1. to each atomic concept A a function AI : ∆I → [0, 1];
2. to each object property R a function RI : ∆I × ∆I → [0, 1];
3. to each individual a an element aI ∈ ∆I such that aI 6= bI if a 6= b (called
Unique Name Assumption, UNA). UNA is often not assumed in DLs.
Let x, y ∈ ∆I be elements of the domain. The fuzzy interpretation function is
extended to complex concepts as follows:
>I (x) = 1
⊥I (x) = 0
I
(¬C) (x) = C I (x)
I
(C u D) (x) = C I (x) ⊗ DI (x)
I
(C t D) (x) = C I (x) ⊕ DI (x)
I
(∀R.C) (x) = inf y∈∆I {RI (x, y) ⇒ C I (y)}
I
(∃R.C) (x) = supy∈∆I {RI (x, y) ⊗ C I (y)}
I
(∃R.{a}) (x) = RI (x, aI ) .
The satisfiability of axioms is then defined by the following conditions:
1. I satisfies ha :C, αi if C I (aI ) ≥ α;
2. I satisfies h(a, b) :R, αi if RI (aI , bI ) ≥ α;
3. I satisfies hC v D, αi if inf x∈∆I {C I (x) ⇒ DI (x)} ≥ α.
Exceptionally, Zadeh fuzzy DLs use Zadeh implication in the semantics of GCIs,
since Kleene-Dienes implication produce some counter-intuitive effects [4]. Note
that classical ALCB is a particular case of this fuzzy ALCB. Finally, I is a model
of K iff I satisfies each axiom in K.
3
http://www.straccia.info/software/FuzzyOWL/ontologies/FuzzyWine.1.0.owl
Reasoning tasks. Let K be a fuzzy KB, C, D be fuzzy concepts, and α a degree
of truth. We can define the following reasoning tasks:
– Consistency. K is consistent iff it has a model, i.e., there is a fuzzy interpre-
tation I satisfying every axiom in K.
– Entailment: K entails an axiom hτ, αi iff every model of K satisfies hτ, αi.
– Concept satisfiability. C is satisfiable to at least degree α (or α-satisfiable)
w.r.t. K iff there is a model I of K such that C I (x) ≥ α for some x ∈ ∆I .
– Concept subsumption. D subsumes C to at least degree α (or α-subsumes)
w.r.t. K iff every model of K satisfies the axiom hC v D, αi.
– Best entailment degree (BED). The BED (also called greatest lower bound)
of an axiom φ ∈ {a :C, (a, b) :R, C v D} w.r.t. K is defined as bed(K, φ) =
sup{α : K |= hφ, αi}, where sup ∅ = 0.
As usual in DLs and fuzzy DLs, reasoning tasks are often mutually inter-definable
and each of the previous tasks can be reduced to the BED. For instance:
– K is not consistent iff bed(K, a :⊥) = 1, where a is new individual. Recall
that inconsistent ontologies entail everything.
– K entails hτ, αi iff bed(K, τ ) ≥ α.
– C is α-satisfiable w.r.t. K iff K ∪ {ha :C, αi} is consistent, where a is new
individual. Note that consistency has already been reduced to the BED.
– D α-subsumes C w.r.t. K iff bed(K, C v D) ≥ α.
3 A MILP-based Reasoning Algorithm for ALCB
It has recently been shown that reasoning is undecidable for several fuzzy DLs in
the presence of GCIs. This is the case e.g. in Lukasiewicz [17] and Product fuzzy
DLs [1]. However, this is not the case in Zadeh DLs or in Lukasiewicz DLs with
an acyclic TBox [17]. In the following, we will restrict to fuzzy KBs with acyclic
TBoxes in classical, Zadeh and Lukasiewicz ALCB. Note that it is enough to
study the BED of a concept assertion since bed(K, (a, b) :R) = bed(K, a :∃R.{b})
and, in our case, bed(K, C v D) = bed(K, a : ¬C t D) for a new individual a.
Our algorithm starts by applying some tableau rules that decompose complex
concept expressions into simpler ones but also generate a system of inequation
constraints [31,33]. These inequations have to hold in order to respect the seman-
tics of the DL constructors. After all rules have been applied, an optimisation
problem must be solved before obtaining the final solution. This problem has
a solution iff the fuzzy KB is consistent. In our case, we will end up with a
bounded Mixed Integer Linear Programming [20] (MILP) problem, although in
other fuzzy DLs Non Linear optimisation problems can be obtained. A MILP
problem consists in minimizing a linear function with respect to a set of con-
straints that are linear inequations in which rational and integer variables can
occur. In our case, MILP problems will be a bounded with rational variables
ranging over [0, 1] and integer variables ranging over {0, 1}.
We can assume without loss of generality that role assertions h(a, b) :R, αi are
replaced by concept assertions ha :∃R.{b}, αi, and that concepts are in Negation
Normal Form (NNF), where the negation only appears before an atomic concept
or an individual value restriction. In fact, a fuzzy concept ¬C can be transformed
into NNF by recursively applying these definitions: nnf(¬A) = ¬A, nnf(¬>) =
⊥, nnf(¬⊥) = >, nnf(¬¬C) = C, nnf(¬(CuD)) = ¬Ct¬D, nnf(¬(CtD)) = ¬Cu
¬D, nnf(¬∀R.C) = ∃R.¬C, nnf(¬∃R.C) = ∀R.¬C, nnf(¬∃R.{a}) = ¬∃R.{a}.
Algorithm 1 shows how to compute bed(K, a :C). Essentially, we consider an
expression of the form ha :¬C, 1 − xi, where x is a [0, 1]-valued variable; this
implies (a :C)I ≤ x. Then, we apply some satisfiability preserving tableau rules
and minimise the original variable x such that all constraints are satisfied, that
is, bed(a :C, K) := inf x such that K ∪ {ha :¬C, 1 − xi} is consistent [7].
Our algorithm use completion-forests since an ABox might contain individ-
uals with arbitrary roles connecting them. A completion-forest F for K is a
collection of trees whose distinguished roots are arbitrarily connected by edges.
– Each node v is labeled with a set L(v) containing ALCB concepts C or
expressions of the forms {o} and ¬{o}. If C ∈ L(v), we consider a variable
xv :C meaning that v is an instance of C to degree greater than or equal to
than the value of the variable xv :C . A novelty of this algorithm is the fact
that if {o} ∈ L(v) then we consider a binary variable xv :{o} . The intuition is
that xv :{o} = 1 iff v is interpreted as individual o. Similarly, if ¬{o} ∈ L(v)
then we consider a binary variable xv :¬{o} with the opposite meaning, i.e.,
xv :¬{o} = 1 iff v is not interpreted as individual o.
– Each edge hv, wi is labeled with a set L(hv, wi) of roles R and if R ∈ L(hv, wi)
then we consider a variable x(v,w):R representing the degree of being hv, wi
and instance of R.
A node v containing some {a} ∈ L(v) is called a nominal node. Specifically,
if {a} ∈ L(v) then v is called an a-nominal node. Note that for a nominal
node v, L(v) may contain several {ai } and ¬{aj }, for 1 ≤ i, j ≤ n, where n
is the number of individuals occurring in K. For example we can have L(v) =
{{a1 }, {a2 }, ¬{a3 }, ¬{a4 }}. The notion of successor is needed when dealing with
edges. A node w is an R-successor of node v if R ∈ L(hv, wi).
We associate to the forest a set CF of constraints of the form l ≤ l0 , l =
l , xi ∈ [0, 1], yi ∈ {0, 1}, where l, l0 are linear expressions using the variables
0
occurring in the forest. F is then expanded by repeatedly applying the tableau
rules in Table 2. Each rule instance is applied at most once, and the rules (N2),
(N3) have the lowest priority. This means that they can only be applied when
no other rule can be applied, right before solving the MILP problem, and hence
the node v has to be one of the ai .
Let us explain Algorithm 1. Firstly, Line 1 adds to the fuzzy KB the assertion
ha :¬C, 1 − xi, involving the variable x that will be minimized. Then, there is
some preprocessing: lines 2-4 transform the concepts into NNF, lines 5-7 replace
the role assertions with equivalent value restrictions, and lines 8-13 initialise the
forest from the axioms in the fuzzy KB by creating a nominal node for each
individual. Then, Lines 14-17 apply the tableau rules until no other rule can
be applied. Next, lines 18-27 introduce some additional constraints stating the
range of each variable ([0, 1] or {0, 1}). Finally, lines 28-33 return the minimised
value of x if the optimisation problem has a solution; or a value 1 otherwise.
Algorithm 1 Computing bed(a0 :C0 , K) in fuzzy ALCB.
Input: A concept assertion a0 :C0 , a fuzzy KB K
Output: BED of a0 :C0 with respect to K
1: K ← K ∪ {ha0 :nnf(¬C0 ), 1 − xi}
2: for each concept assertion ha :C, αi ∈ K do
3: K ← (K \ {ha :C, αi}) ∪ {ha :nnf(C), αi}
4: end for
5: for each role assertion h(a, b) :R, αi ∈ K do
6: K ← (K \ {h(a, b) :R, αi}) ∪ {ha :∃R.{b}, αi}
7: end for
8: create an empty forest F
9: CF := ∅
10: for each individual a occurring in K do
11: create a node v
12: L(v) := L(v) ∪ {{a}}
13: end for
14: repeat
15: apply a rule in Table 2 to a node v
16: mark the applied rule as not applicable anymore to node v
17: until no more rule can be applied to nodes in F
18: for each variable of the form xv :C ∈ K do
19: if the logic is Lukasiewicz or Zadeh ALCB then
20: CF := CF ∪ {xv :C ∈ [0, 1]}
21: else
22: CF := CF ∪ {xv :C ∈ {0, 1}}
23: end if
24: end for
25: for each variable z ∈ K of the forms y, xv :{o} , xv :¬{o} do
26: CF := CF ∪ {z ∈ {0, 1}}
27: end for
28: if CF has a solution then
29: solve the optimisation problem on x
30: return x
31: else
32: return 1
33: end if
Table 2. Rules for fuzzy ALCB with an acyclic TBox.
(>) IF > ∈ L(v) THEN CF := CF ∪ {xv:> = 1}.
(⊥) IF ⊥ ∈ L(v) THEN CF := CF ∪ {xv:⊥ = 0}.
(Ā) IF ¬A ∈ L(v) THEN
1. L(v) = L(v) ∪ {A}
2. CF := CF ∪ {xv:A ≤ 1 − xv:¬A }
(u) IF C1 u C2 ∈ L(v) THEN
1. L(v) = L(v) ∪ {C1 , C2 }
2. CF := CF ∪ {xv:C1 ⊗ xv:C2 ≥ xv:C1 uC2 }
(t) IF C1 t C2 ∈ L(v) THEN
1. L(v) = L(v) ∪ {C1 , C2 }
2. CF := CF ∪ {xv:C1 ⊕ xv:C2 ≥ xv:C1 tC2 }
(∀) IF ∀R.C ∈ L(v) AND w is an R-successor of v THEN
1. L(w) = L(w) ∪ {C}
2. CF := CF ∪ {xv:∀R.C ≤ x(v,w):R ⇒ xw:C }
(∃) IF ∃R.C ∈ L(v) AND C 6= {a} THEN
1. create a new node w
2. L(hv, wi) = L(hv, wi) ∪ {R}
3. L(w) = L(w) ∪ {C}
4. CF := CF ∪ {xw:C ⊗ x(v,w):R ≥ xv:∃R.C }.
(v) IF hA v C, αi ∈ T AND A ∈ L(v) THEN
1. L(v) = L(v) ∪ {C}
2. CF := CF ∪ {xv:A ⇒ xv:C ≥ α}
(=) IF A = C ∈ T AND A ∈ L(v) THEN
1. L(v) = L(v) ∪ {C}
2. CF := CF ∪ {xv:A = xv:C }
(¬ =) IF A = C ∈ T AND ¬A ∈ L(v) THEN
1. L(v) = L(v) ∪ {¬C}
2. CF := CF ∪ {xv:¬A = xv:¬C }
(Ass). IF ha :C, αi ∈ K AND v is an a-nominal node THEN
1. L(v) = L(v) ∪ {C}
2. CF := CF ∪ {xv :{a} ⇒ xv :C ≥ α}
(∀o ) IF ¬∃R.{a} ∈ L(v) AND w is an R-successor of v THEN
1. L(w) = L(w) ∪ {¬{a}}
2. CF := CF ∪ {xv:¬∃R.{a} ≤ x(v,w):R ⇒ xw:¬{a} }.
(∃o ) IF ∃R.{a} ∈ L(v) AND w is an a-nominal node THEN
1. L(hv, wi) = L(hv, wi) ∪ {R}
2. CF := CF ∪ {xw:{a} ⇒ (xv:∃R.{a} ⇒ x(v,w):R ) ≥ 1}.
(N1) IF ¬{a} ∈ L(v) THEN
1. L(v) = L(v) ∪ {{a}}
2. CF := CF ∪ {xv:¬{a} = 1 − xv:{a} }.
(N2) IF {{a1 }, . . . , {an }} ⊆ L(v) with n ≥ 2 AND no other rule can be applied
THEN CF := CF ∪ {xv:{a1 } + . . . + xv:{an } ≤ 1}.
(N3) IF {a} ∈ L(vi ), for 1 ≤ i ≤ n AND no other rule can be applied THEN
CF := CF ∪ {xv1 :{a} + . . . + xvn :{a} = 1}.
Now, let us explain the rationale behind the rules. Rules (>), (⊥), (Ā), (u), (t),
(∀), (∃), (v), (=), and (¬ =) have directly been derived from [17,31], so we do
not comment them further.
According to the (Ass) rule, given an axiom ha :C, αi and an a-nominal node
v, we add C to L(v) and then add the constraint xv :{a} ⇒ xv :C ≥ α to
CF . Since xv :{a} is binary, this is equivalent to say that either xv :{a} = 0 or
xv :C ≥ α. That is, if v is interpreted as a, then v must belong to concept C with
at least degree α. Notice that we apply the rule not only to the nominal nodes
created during the initialisation phase, but also to all nominal nodes created
during the inference process. (∀o ) and (∃o ) are similar to the rules managing
universal restrictions and existential restrictions. Note that in the (∃o ) rule, the
equation xw:{a} ⇒ (xv:∃R.{a} ⇒ x(v,w):R ) ≥ 1 encodes the fact that if node w is
interpreted as individual a then indeed the truth value of x(v,w):R has to be at
least the truth value of xv:∃R.{a} .
(N1) avoids the inconsistency of having a node both interpreted and not
interpreted as the same individual. (N2) deals with the UNA, and guarantees
that a nominal node is not interpreted as more than one individual of the ai ∈
L(v). Finally, (N3) makes sure that for every a-nominal node in the forest there
is exactly one node interpreted as the individual a.
Concerning the MILP encoding of the fuzzy operators for classical, Lukasiewicz
and Zadeh logics, we use the same ideas in e.g. [17,33]. Specifically, x1 ⇒ x2 ≥ z
can be encoded as (denoted 7→) {1−x1 ⊕x2 ≥ z}. In Lukasiewicz, x1 ⊕x2 ≥ z 7→
{x1 + x2 ≥ z}, while x1 ⊗ x2 ≥ z 7→ {y ≤ 1 − z, x1 + x2 − 1 ≥ z − y, y ∈ {0, 1}},
where y is a new variable. In Zadeh, x1 ⊗ x2 ≥ z 7→ {x1 ≥ z, x2 ≥ z}, while
x1 ⊕ x2 ≥ z 7→ {z ≥ x1 , z ≥ x2 , x1 + y ≥ z, x2 + (1 − y) ≥ z, y ∈ {0, 1}}, where
y is a new variable. For classical DLs, any of the previous encodings is valid as
long as we additionally force x1 , x2 to be binary. It is convenient to chose those
encodings that minimise the number of new variables.
Soundness, completeness, and termination can be proved similarly as in [17]:
Proposition 1. Given a fuzzy KB K in Lukasiewicz, Zadeh, and classical ALCB
with an acyclic TBox, Algorithm 1 terminates and correctly computes bed(K, a :C).
4 A Running Example
Example 2. Consider the fuzzy KB K = {b :A, c :B, a :∃R.{b} t ∃R.{c}} and let
us show (the chosen fuzzy logic is irrelevant) that
bed(K, a :∃R.A t ∃R.{c}) = 1
The axioms of K are already in NNF and there are no role assertions. Fur-
thermore, to compute bed(K, a :∃R.A t ∃R.{c}), the axiom
ha :∀R.¬A u ¬∃R.{c}, 1 − xi (1)
is added to K. The forest initialisation creates three nodes v1 , v2 , and v3 being
a b-nominal, c-nominal and a-nominal, respectively.
At first, the (Ass) rule is applied and, thus,
1. A is added to L(v1 );
2. B is added to L(v2 );
3. ∃r.{b} t ∃r.{c} and ∀R.¬A u ¬∃R.{c} are added to L(v3 );
4. CF contains so far expressions of the form xv:{a} ⇒ xv:C ≥ α, namely
xv1 :{b} ⇒ xv1 :A ≥ 1
xv2 :{c} ⇒ xv2 :B ≥ 1
xv3 :{a} ⇒ xv3 :∃R.{b}t∃R.{c} ≥ 1
xv3 :{a} ⇒ xv3 :∀R.¬Au¬∃R.{c} ≥ 1 − x .
Next, the (t) is applied to v3 and, thus,
1. ∃R.{b} and ∃R.{c} are added to L(v3 );
2. xv3 :∃R.{b} ⊕ xv3 :∃R.{c} ≥ xv3 :∃R.{b}t∃R.{c} is added to CF .
Then, the (u) rule is applied to v3 and, thus,
1. ∀R.¬A and ¬∃R.{c} are added to L(v3 );
2. xv3 :∀R.¬A ⊗ xv3 :¬∃R.{c} ≥ xv3 :∀R.¬Au¬∃R.{c} is added to CF .
Next, we apply the (∃o ) rule to ∃R.{b} ∈ L(v3 ) and, thus,
1. R is added to L(hv3 , v1 i);
2. xv1 :{b} ⇒ (xv3 :∃R.{b} ⇒ x(v3 ,v1 ):R ) ≥ 1 is added to CF .
Now we can apply the (∀) rule to L(v3 ) and, thus,
1. ¬A is added to L(v1 );
2. xv3 :∀R.¬A ≤ x(v3 ,v1 ):R ⇒ xv1 :¬A is added to CF .
After that, we can apply the (∀o ) rule to L(v3 ) and, thus,
1. ¬{c} is added to L(v1 );
2. xv3 :¬∃R.{c} ≤ x(v3 ,v1 ):R ⇒ xv1 :¬{c} is added to CF .
Then, the (N 1) rule adds {c} to L(v1 ) and xv1 :¬{c} = 1 − xv1 :{c} to CF . Since
v1 is also a c-nominal node now, we may apply the (Ass) rule to it, so
1. B is added to L(v1 );
2. xv1 :{c} ⇒ xv1 :B ≥ 1 is added to CF .
The (∃o ) rule is applied next to ∃R.{c} ∈ L(v3 ) and, thus,
1. R is added to L(hv3 , v2 i);
2. xv1 :{c} ⇒ (xv3 :∃R.{c} ⇒ x(v3 ,v1 ):R ) ≥ 1 is added to CF ;
3. xv2 :{c} ⇒ (xv3 :∃R.{c} ⇒ x(v3 ,v2 ):R ) ≥ 1 is added to CF .
As now node v2 has become an R-successor of v3 , we may apply the (∀) and (∀o )
rules to L(v3 ) and, thus,
1. ¬A is added to L(v2 );
2. xv3 :∀R.¬A ≤ x(v3 ,v2 ):R ⇒ xv2 :¬A is added to CF ;
3. ¬{c} is added to L(v2 );
4. xv3 :¬∃R.{a} ≤ x(v3 ,v2 ):R ⇒ xv2 :¬{c} is added to CF .
The (N 1) rule adds now adds {c} to L(v2 ) and xv2 :¬{c} = 1 − xv2 :{c} to CF .
Eventually, rule (N 2) and (N 3) add the following constraints to CF :
1. xv1 :{b} + xv1 :{c} ≤ 1;
2. xv3 :{a} = 1;
3. xv1 :{b} = 1;
4. xv1 :{c} + xv2 :{c} = 1.
Finally, we have to determine the minimal value of x such that CF is satisfi-
able. Therefore, from the last equations, we get immediately that xv1 :{b} = 1,
xv3 :{a} = 1, xv1 :{c} = 0, and xv2 :{c} = 1. Of course, then xv2 :¬{c} = 0 and
xv1 :¬A = 0. The assertion a :∃R.{b} t ∃R.{c} implies that xv3 :∃R.{b} = 1 or
xv3 :∃R.{c} = 1. If xv3 :∃R.{b} = 1 then from xv1 :{b} ⇒ (xv3 :∃R.{b} ⇒ x(v3 ,v1 ):R ) ≥ 1
we get that x(v3 ,v1 ):R = 1, while if xv3 :∃R.{c} = 1 from xv2 :{c} ⇒ (xv3 :∃R.{c} ⇒
x(v3 ,v2 ):R ) ≥ 1 we get that x(v3 ,v2 ):R = 1. Now, suppose x < 1. From Equa-
tion 1, xv3 :∀R.¬Au¬∃R.{c} > 0, and thus xv3 :∀R.¬A > 0 and xv3 :¬∃R.{c} > 0. If
x(v3 ,v1 ):R = 1, we get a contradiction with xv1 :¬A = 0, while if x(v3 ,v2 ):R = 1, we
get a contradiction with xv2 :¬{c} = 0. However, for x = 1 CF is satisfiable, so
our algorithm returns x = 1. Indeed, bed(K, a :∃R.A t ∃R.{c}) = 1 holds.
5 Conclusions and Future Work
In this paper we have proposed the first algorithm based on OR to reason with
fuzzy DLs including individual value restrictions. In particular, we have proposed
an algorithm to compute the BED in classical, Zadeh, and Lukasiewicz ALCB
if the TBox is acyclic. The algorithm could be extended to the case of general
TBoxes using blocking. A relevant property of the algorithm is that only one
optimisation problem has to be solved, deferring the inherent non-determinism
in ALCB to the optimisation problem solver.
Future work will include the extension of the algorithm to more expressive
fuzzy DLs, such as SHIF B(D). Up to know, SHIF(D) is current the most ex-
pressive fuzzy DL for which there is an implementation of an OR-algorithm (the
fuzzyDLsystem). On the one hand, adding inverse roles to the language seems
challenging because of the possibility of having inverse functional role axioms.
On the other hand, it would also be interesting to have unrestricted nominals
to arbitrarily form complex concept expressions. Another possible extension is
considering fuzzy nominals of the form {α/o} that can be used to describe fuzzy
sets by enumeration of their elements [4].
Last but not least, we are aware that the current proposal is not optimal
in the handling of nominal nodes, as several a-nominal nodes may occur in a
completion-forest. We plan to adapt and implement the well-known node merging
technique developed for classical DLs, such as for SHOIQ [24], to the fuzzy
case as well, analyse the overall computational complexity and experiment the
algorithm within fuzzyDL.
References
1. F. Baader, S. Borgwardt, and R. Peñaloza. On the decidability status of fuzzy
ALC with general concept inclusions. Journal of Philosophical Logic, In press.
2. F. Baader, D. Calvanese, D. McGuinness, D. Nardi, and P. F. Patel-Schneider, edi-
tors. The Description Logic Handbook: Theory, Implementation, and Applications.
Cambridge University Press, 2003.
3. T. Berners-Lee, J. Hendler, and O. Lassila. The semantic web. The Scientific
American, 284(5):34–43, 2001.
4. F. Bobillo, M. Delgado, and J. Gómez-Romero. Crisp representations and rea-
soning for fuzzy ontologies. International Journal of Uncertainty, Fuzziness and
Knowledge-Based Systems, 17(4):501–530, 2009.
5. F. Bobillo, M. Delgado, J. Gómez-Romero, and U. Straccia. Fuzzy description
logics under Gödel semantics. International Journal of Approximate Reasoning,
50(3):494–514, 2009.
6. F. Bobillo, M. Delgado, J. Gómez-Romero, and U. Straccia. Joining Gödel and
Zadeh fuzzy logics in fuzzy description logics. International Journal of Uncertainty,
Fuzziness and Knowledge-Based Systems, 20:475–508, 2012.
7. F. Bobillo and U. Straccia. fuzzyDL: An expressive fuzzy description logic rea-
soner. In Proceedings of the 17th IEEE International Conference on Fuzzy Systems
(FUZZ-IEEE 2008), pages 923–930, June 2008.
8. F. Bobillo and U. Straccia. Fuzzy description logics with general t-norms and
datatypes. Fuzzy Sets and Systems, 160(23):3382–3402, 2009.
9. F. Bobillo and U. Straccia. Fuzzy ontology representation using OWL 2. Interna-
tional Journal of Approximate Reasoning, 52:1073–1094, 2011.
10. F. Bobillo and U. Straccia. Reasoning with the Lukasiewicz fuzzy description logic
SROIQ. Information Sciences, 181:758–778, 2011.
11. F. Bobillo and U. Straccia. Aggregation operators for fuzzy ontologies. Applied
Soft Computing, 13:3816–3830, 2013.
12. S. Borgwardt, F. Distel, and R. Peñaloza. How fuzzy is my fuzzy description
logic? In B. Gramlich, D. Miller, and U. Sattler, editors, Proceedings of the 6th
International Joint Conference on Approximated Reasoning (IJCAR 2012), volume
7364 of Lecture Notes in Artificial Intelligence, pages 82–96. Springer-Verlag, 2012.
13. S. Borgwardt, F. Distel, and R. Peñaloza. Decidable Gödel description logics
without the finitely-valued model property. In Proceedings of the 14th International
Conference on Principles of Knowledge Representation and Reasoning (KR 2014).
AAAI Press, 2014.
14. S. Borgwardt and R. Peñaloza. The complexity of lattice-based fuzzy description
logics. Journal on Data Semantics, 2(1):1–19, 2013.
15. S. Borgwardt and R. Peñaloza. Consistency reasoning in lattice-based fuzzy de-
scription logics. International Journal of Approximate Reasoning, In press.
16. M. Cerami, A. Garcı́a-Cerdaña, and F. Esteva. On finitely-valued fuzzy description
logics. International Journal of Approximate Reasoning, In press.
17. M. Cerami and U. Straccia. On the (un)decidability of fuzzy Description Logics
under Lukasiewicz t-norm. Information Sciences, 227:1–21, 2013.
18. B. Cuenca-Grau, I. Horrocks, B. Motik, B. Parsia, P. F. Patel-Schneider, and
U. Sattler. OWL 2: The next step for OWL. Journal of Web Semantics, 6(4):309–
322, 2008.
19. A. Garcı́a-Cerdaña, E. Armengol, and F. Esteva. Fuzzy Description Logics and
t-norm based fuzzy logics. International Journal of Approximate Reasoning,
51(6):632–655, 2010.
20. M. K. H. Salkin. Foundations of Integer Programming. North-Holland, 1988.
21. P. Hájek. Metamathematics of Fuzzy Logic. Kluwer, 1998.
22. P. Hájek. Making fuzzy description logic more general. Fuzzy Sets and Systems,
154(1):1–15, 2005.
23. I. Horrocks, O. Kutz, and U. Sattler. The even more irresistible SROIQ. In
Proceedings of the 10th International Conference on Principles of Knowledge Rep-
resentation and Reasoning (KR 2006), pages 57–67. AAAI Press, 2006.
24. I. Horrocks and U. Sattler. A tableau decision procedure for SHOIQ. Journal of
Automated Reasoning, 39(3):249–276, 2007.
25. T. Lukasiewicz and U. Straccia. Managing uncertainty and vagueness in description
logics for the semantic web. Journal of Web Semantics, 6:291–308, 2008.
26. T. P. Mailis, G. Stoilos, N. Simou, G. B. Stamou, and S. D. Kollias. Tractable rea-
soning with vague knowledge using fuzzy EL++ . Journal of Intelligent Information
Systems, 39:399–440, 2012.
27. P. S. Mostert and A. L. Shields. On the structure of semigroups on a compact
manifold with boundary. Annals of Mathematics, 65(1):117–143, 1957.
28. G. Stoilos and G. Stamou. Reasoning with fuzzy extensions of OWL and OWL 2.
Knowledge and Information Systems, In press.
29. G. Stoilos, G. Stamou, J. Z. Pan, V. Tzouvaras, and I. Horrocks. Reasoning with
very expressive fuzzy description logics. Journal of Artificial Intelligence Research,
30(8):273–320, 2007.
30. U. Straccia. Reasoning within fuzzy description logics. Journal of Artificial Intel-
ligence Research, 14:137–166, 2001.
31. U. Straccia. Description logics with fuzzy concrete domains. In Proceedings of
the 21st Conference on Uncertainty in Artificial Intelligence (UAI 2005), pages
559–567. AUAI Press, 2005.
32. U. Straccia. A fuzzy description logic for the semantic web. In E. Sanchez, editor,
Fuzzy Logic and the Semantic Web, Capturing Intelligence, chapter 4, pages 73–90.
Elsevier, 2006.
33. U. Straccia. Foundations of Fuzzy Logic and Semantic Web Languages. CRC
Studies in Informatics Series. Chapman & Hall, 2013.
34. J. Yen. Generalizing term subsumption languages to fuzzy logic. In Proceedings
of the 12th International Joint Conference on Artificial Intelligence (IJCAI 1991),
pages 472–477, Sydney, Australia, 1991.
35. L. A. Zadeh. Fuzzy sets. Information and Control, 8(3):338–353, 1965.