=Paper=
{{Paper
|id=Vol-423/paper-1
|storemode=property
|title=Deciding Fuzzy Description Logics by Type Elimination
|pdfUrl=https://ceur-ws.org/Vol-423/paper1.pdf
|volume=Vol-423
|dblpUrl=https://dblp.org/rec/conf/semweb/KellerH08
}}
==Deciding Fuzzy Description Logics by Type Elimination==
https://ceur-ws.org/Vol-423/paper1.pdf
Deciding Fuzzy Description Logics by
Type Elimination!
Uwe Keller1 and Stijn Heymans2
1
Semantic Technology Institute (STI) Innsbruck, University of Innsbruck, Austria.
eMail: uwe.keller@sti2.at
2
Knowledge-based Systems Group, Institute of Information Systems, Vienna University of
Technology, Austria. eMail: heymans@kr.tuwien.ac.at
Abstract. We present a novel procedure FixIt(ALC) for deciding knowledge
base satisfiability in the Fuzzy Description Logic (FDL) ALC. FixIt(ALC)
does not search for tree-structured models as in tableau-based proof procedures,
but embodies a fixpoint-computation of canonical models that are not necessar-
ily tree-structured. Conceptually, the procedure is based on a type-elimination
process. Soundness, completeness and termination are proven. To the best of our
knowledge it is the first fixpoint-based decision procedure for FDLs, hence intro-
ducing a new class of inference procedures into FDL reasoning.
1 Introduction
Description Logics (DLs) [1] are a popular family of formally well-founded and decid-
able knowledge representation languages. DLs have a wide range of applications, e.g.,
they form the basis for Semantic Web (SW) ontology languages used such as OWL [7].
Fuzzy Description Logics (FDLs) [13] extend DLs to represent vague concepts and
relations, and as such are very well suited to cover for representing and reasoning
with uncertainty, a requirement that naturally arises in many practical applications of
knowledge-based systems, in particular the SW.
So far, reasoning in Fuzzy DLs is mainly based on tableau-methods (e.g. [13,12,4,11,16,3]).
Further, [14] demonstrates how to use inference procedures for classical DLs to perform
reasoning in (some) FDLs. Still, reasoning in FDLs is at least as hard as reasoning in
classical (crisp) DLs. Even in DLs of modest expressivity (e.g. ALC [13,14,12] the
fuzzy variant of the DL ALC [10]) the worst-case complexity of reasoning is signif-
icant even in restricted cases [13]. Therefore, it is clear that there can not be a single
inference method that works well on all problems.
Consequently, our goal is to enrich the range of available methods for reasoning
with FDLs with a fundamentally different approach. In practical applications of DLs
(and hence FDLs) a particularly important feature for representing domain models is
the support of so-called general terminologies (see e.g. [12]), i.e., the possibility to cap-
ture (potentially recursive) interdependencies between complex concepts in a domain
!
This work has been partially funded by the European Commission under the LarKC project
(FP7 - 215535). Stijn Heymans is supported by the Austrian Science Fund (FWF) under
projects P20305 and P20840.
model. However, besides the tableau-based methods for DLs (e.g [12,4,16,3]) there are
at present no other FDL inference methods which can deal with general terminologies.
We want to provide an alternative to tableau-based methods that can deal with general
terminologies.
The main contributions of the paper are as follows:
− We present a novel procedure FixIt(ALC) (cf. Section 3) for deciding knowledge
base (KB) satisfiability in the FDL ALC (cf. Section 2).
− We formally prove soundness, completeness and termination of the algorithm (cf.
Section 3).
− FixIt(ALC) generalizes a type-elimination-based decision procedure [8] for the
(classical) modal logic K (i.e. KBDD [6]) to the FDL ALC. Additionally we inte-
grate (fuzzy) ABoxes and general TBoxes which are not dealt with in KBDD.
− To the best of our knowledge it is the first fixpoint-based decision procedure that
has been proposed for FDL introducing a new class of inference procedures into
FDL reasoning.
− Besides the tableau-based methods in [12,4,16,3], it is the only approach to inte-
grate general terminologies in FDL reasoning and the first non-tableau-based one
that we are aware of. General terminologies are handled in a fundamentally differ-
ent way than in standard tableau-based method such as [12,4].
Our method is interesting especially regarding the last aspect since the handling of gen-
eral terminologies in standard tableau-based methods (e.g. [12,4]) is a major source of
non-determinism and thus computational inefficiency. In our case no non-deterministic
choice is introduced by terminologies.
2 Preliminaries
We introduce ALC [13], the fuzzy variant of the Description Logic ALC [10] (the latter
can be seen as a syntactic variant of the multi-modal logic K(m) [9]). ALC provides the
starting point for more expressive FDLs [15] that have been proposed to fuzzify major
fragments of OWL [7].
Syntax. Concept expressions are constructed from a signature Σ = (C, R, I) with
concept names C, role names R, and individual names I. The set of concept expres-
sions C(Σ) over Σ is defined as the smallest set of expressions that contains C, "
and is closed under the application of the concept constructors C # D (intersection),
C $ D (union), ¬C (complement), and ∀R.C (universal role restriction) for R ∈ R
and C, D ∈ C(Σ) . We allow expressions ∃R.C for C ∈ C(Σ), R ∈ R and ⊥ and
treat them as shortcuts for ¬∀R.¬C and ¬" respectively. A TBox axiom (or general
concept inclusion axiom (GCI)) is an expression of the form C ) D s.t. C, D ∈ C(Σ).
A terminology (or TBox) T is a finite set of TBox axioms. Syntactically, the vagueness
of descriptions becomes explicit only when describing specific instances and their inter-
relations: a (fuzzy) ABox axiom is either a *i : C "# d+ or a *R(i, i! ) ≥ d+ s.t. i, i! ∈ I,
d ∈ [0, 1], and "#∈ {≤, ≥, =}. An ABox A is a finite set of ABox axioms. Finally, a
knowledge base K = (T , A) consists of a TBox T and an ABox A. Let IndA ⊆ I de-
note the individual names that occur in A. We denote the set of all concept expressions
that occur as subexpressions in K by sub(K).
Semantics. Semantically, vagueness is reflected in the use of fuzzy sets and relations
when interpreting concepts and roles: an interpretation I = (∆I , ·I ) consists of a non-
empty set ∆I called the domain, and a function ·I which maps each concept name
C ∈ C to a fuzzy set C I : ∆I → [0, 1], each role name R ∈ R to a fuzzy relation
RI : ∆I × ∆I → [0, 1] and each individual name i ∈ I to an element iI ∈ ∆I . The
interpretation function ·I is extended to arbitrary concept expressions C ∈ C(Σ) as
follows:
– (C # D)I (o) = min(C I (o), DI (o))
– (C $ D)I (o) = max(C I (o), DI (o))
– (¬C)I (o) = 1 − C I (o)
– (∀R.C)I (o) = inf o! ∈∆I {max(1 − RI (o, o! ), C I (o! ))}
– "I (o) = 1
for all o ∈ ∆I , C, D ∈ C(Σ), R ∈ R.
An interpretation I satisfies a TBox axiom α = C ) D iff. for all o ∈ ∆I it
holds that C I (o) ≤ DI (o), i.e. C is a fuzzy subset of D. I satisfies an ABox axiom
α = *i : C "# d+ iff. C I (iI ) "# d. I satisfies an ABox axiom α = *R(i, i! ) ≥ d+ iff.
RI (iI , i!I ) ≥ d. In all these cases, we write I |= α. I satisfies a TBox T (or is a model
of T ) iff. I |= α for all α ∈ T . I satisfies an ABox A (or is a model of A) iff. I |= α
for all α ∈ A. Finally, I satisfies a knowledge base K = (T , A) (or is a model of K)
iff. I |= T and I |= A.
Reasoning in ALC. Given a fuzzy KB K = (T , A), fuzzy ABox axioms or GCIs α and
concept expressions C, D ∈ C(Σ), we can analyze particular semantic characteristics
and interdependencies: We say that K is satisfiable (or consistent) iff. there is a model
I for K. K entails α (denoted as K |= α) iff. all models I of K satisfy α. Concept C is
subsumed by concept D (wrt. a KB K) iff. K |= C ) D. Two concepts C and D are
called equivalent (wrt. a KB K) iff. for any model I of K it holds that C I (o) = DI (o)
for all o ∈ ∆I . Two concepts C and D are called disjoint (wrt. a KB K) iff. for any
model I of K it holds that there does not exists an o ∈ ∆I such that C I (o) > 0 and
DI (o) > 0. A concept C is called satisfiable (wrt. a KB K) iff. there exists a model I of
T such that C I (o) > 0 for some o ∈ ∆I . Further, one might want to compute the truth
value bounds for a given ABox assertion α wrt. K to determine the possibility interval
that is enforced for α by the background knowledge in K: The greatest lower bound of
α wrt. K is defined as glb(α, K) := sup{d ∈ [0, 1] | K |= *α ≥ d+} and the least upper
bound of α wrt. K is defined as lub(α, K) := inf {d ∈ [0, 1] | K |= *α ≤ d+} (where
sup ∅ = inf ∅ = 0). Computing glb(α, K) and lub(α, K) is usually called the best truth
value bounds (BTVB) problem.
One of the most fundamental reasoning problems is to determine whether a given fuzzy
KB K is satisfiable. A lot of other reasoning tasks (e.g., checking for concept satisfi-
ability wrt. a TBox, entailment of fuzzy ABox assertions, or the BTVB problem) can
be reduced to KB satisfiability checking (cnf. [13]) and therefore solved by a respec-
tive decision procedure. For this reason, we consider KB satisfiability as the reasoning
problem to be solved.
3 Fixpoint-based Decision Procedure
We present a decision procedure for KB satisfiability in ALC which does not rely on
systematic search in the first place (as e.g. tableau-based methods), but instead con-
structs a canonical interpretation by means of a fixpoint construction. The so-constructed
(canonical) interpretation (if non-empty) satisfies the TBox of a KB and allows to de-
rive a model for the given knowledge base K iff. K is satisfiable. In contrast to tableau-
based procedures a canonical interpretation is in general not tree-shaped. Further, it can
be shown that the number of iterations required to reach a fixpoint is linear in the modal
depth of K.
Preprocessing. Without loss of generality, we can restrict ourselves to normalized
knowledge bases, i.e. knowledge bases which contain only fuzzy ABox assertions of
the form *α ≥ d+ [12]. Further, we can assume that all axioms in K are in box normal
form (BNF) [6] (i.e. the only negative concept subexpressions are of the form ¬∀R.C
or negated atomic concept names ¬C).
3.1 Basic Notions and Intuition
Types. Let K = (T , A) denote a normalized ALC knowledge base in BNF. Let sub(K)
denote the set of all concept expressions that occur as subexpressions somewhere in an
axiom in K. The closure of a knowledge base cl(K) is defined as the smallest set of
concept expressions such that for all C ∈ sub(K), if C is not of the form ¬D, then
{C, ¬C} ⊆ cl(K). Further, let PossDeg(K) denote the set of all relevant possibility
degrees that can be derived from K, i.e. PossDeg(K) = {0, 0.5, 1} ∪ {d|*α ≥ d+ ∈
A} ∪ {1 − d|*α ≥ d+ ∈ A}. It has been shown in [13,14] that if K is satisfiable,
then there is as well a model of K which assigns possibility degrees in PossDeg(K)
only. Hence, for our purposes we do not need to consider arbitrary possibility degrees
d ∈ [0, 1], but only the finite set PossDeg(K) that can be derived from K.
The closure cl(K) and the relevant possibility degrees PossDeg(K) together give
us the basic vocabulary to describe individuals and their (fuzzy) properties in inter-
pretations for K. More specifically, the notion of a type allows to represent individ-
uals of an interpretation in a syntactic way: a fuzzy K-type τ is a maximal subset of
cl(K) × PossDeg(K) such that:
1. if *C, d+ ∈ τ and *C, d! + ∈ τ then d = d!
2. if C = ¬C ! then *C, d+ ∈ τ iff. *C ! , 1 − d+ ∈ τ
3. if C = C ! # C !! then *C, d+ ∈ τ iff. *C ! , d! + ∈ τ and *C !! , d!! + ∈ τ and d =
min(d! , d!! )
4. if C = C ! $ C !! then *C, d+ ∈ τ iff. *C ! , d! + ∈ τ and *C !! , d!! + ∈ τ and d =
max(d! , d!! )
5. for all C ) C ! ∈ T : if *C, d+ ∈ τ and *C ! , d! + ∈ τ then d ≤ d!
6. if C = " then *C, 1+ ∈ τ
Since cl(K) and PossDeg(K) are both finite sets, there are at most 2|cl(D)|·|PossDeg(K)|
different K-types. Each type τ can be seen as an individual and syntactically represents
all (fuzzy) properties that can be observed about that individual: *C, d+ ∈ τ represents
the statement that the respective individual τ belongs to concept C with the possibility
degree d. Hence, the set of all K-types (or simply types) provides enough vocabulary
to let us describe all kinds of interpretations for K simply be fixing how to interconnect
individuals (and therefore types).
Canonical Model. It turns out that it is possible to connect types in a fixed (or canon-
ical) way, such that the interconnection defined is consistent with almost all properties
specified syntactically in the type. The interconnections can be derived from the types
themselves:
For a set of types T we can define for each role R a canonical accessibility relation
∆R : T × T → PossDeg(K) that “maximally” interconnects types τ, τ ! ∈ T with
possibility degree d ∈ PossDeg(K): Let δ(d, d! ) := 1 if d ≤ d! and δ(d, d! ) := 1 − d if
d > d! . Then, we can define ∆R by
∆R (τ, τ ! ) := min{δ(d, d! )|*∀R.C, d+ ∈ τ, *C, d! + ∈ τ ! }
if ∀R.C ∈ cl(K) for some C ∈ C, and ∆R (τ, τ ! ) := 1 otherwise.
This way, we can construct a canonical interpretation IT for any given set of types T
using the canonical interconnection of types by ∆R as follows: IT = (T, ·IT ) with (i)
for any (atomic) concept name C in K and any τ ∈ T we set C IT (τ ) = d if *C, d+ ∈ τ ,
and (ii) RIT (τ, τ ! ) = ∆R (τ, τ ! ) for any role R in K and any τ, τ ! ∈ T . Please note,
that by our definition of K-types, IT is well-defined for any concept name or role name.
However, our definition deliberately leaves open the interpretation of individuals. We
therefore define in fact a class of canonical interpretations, each of which fixes a specific
way of how to interpret the individuals in a KB K.
The canonical interconnection in IT is chosen in such a way that all assignments
of possibility degrees to concepts of the form C = ∀R.C ∈ τ are lower bounds for
the possibility degrees that are in fact assigned by a canonical interpretation IT . Hence,
such a canonical interpretation is almost immediately a (canonical) model for the ter-
minology T , i.e. it satisfies that
C IT (τ ) = d iff. *C, d+ ∈ τ (∗)
for almost all C ∈ cl(K) it holds and therefore IT |= C ) C for all C ) C ∈ T
! !
by clause (5) in our definition of K-types. That (∗) is satisfied by IT is straightforward
for the cases of concept names C, or complex concepts of the form C = C ! # C !! ,
C = C ! $ C !! , C = ¬C ! and the C IT (τ ) ≥ d case for C = ∀R.C by our definition
of types and the definition of ∆R . The only cases where (∗) can be violated by IT
is for types τ containing universally role restricted concepts ∀R.C that are assigned a
possibility degree which is too small (wrt. the R-successor types τ ! in IT ) to properly
reflect the semantics of ∀R.C in ALC, i.e. to coincide with the greatest lower bound of
the set
{max(1 − RIT (τ, τ ! ), C IT (τ ! )) | τ ! ∈ T }
Types τ in which the possibility degree assigned d to ∀R.C is too small to be consis-
tent with the semantics of ALC are called bad types. Bad types τ ∈ T can be detected
easily, since they satisfy that there exist R ∈ R, C ∈ C(Σ), d ∈ PossDeg(K) s.t.
*∀R.C, d+ ∈ τ and for all τ ! ∈ T : if *C, d! + ∈ τ ! then max(1 − ∆R (τ, τ ! ), d! ) > d.
This suggest the the following simple algorithm (which uses a fuzzy type elimina-
tion process as its core): in order to compute a maximal interpretation that satisfies all
terminological axioms, we start off with the maximal set of types (i.e all K-types) and
iteratively fix all problems that prevent (∗) from being satisfied by removing bad types.
This way, we must eventually reach a fixpoint after finitely many steps. If the resulting
set of types is non-empty, we know that (∗) must hold (since all problems have been
fixed) and therefore we can be certain that the corresponding canonical interpretation
satisfies T (and covers all other possible models of T at the same time). Hence, we
eventually need to check if all ABox axioms are satisfied by the canonical interpreta-
tion. If this is the case, we have found a model for K, otherwise, we know that there can
not be any interpretation that satisfies both T and A at the same time. In other words,
K is not satisfiable.
Algorithm. The type elimination process sketched above can be formalized as shown
in Fig. 1. Note that the emptiness test for the fixpoint T is covered implicitly: if the
fixpoint T is empty, then the test in the if-statement fails trivially.
procedure satisfiable(K): boolean
T := {τ |τ is a K-type };
repeat
T ! := T ;
T := T ! \ badtypes(T ! );
until T = T ! ;
if there exists a total function π : IndA → T s.t. "C, d! # ∈ π(o) and d ≤ d! for each
"o : C ≥ d# ∈ A, and ∆R (π(o), π(o! )) ≥ d for each "R(o, o! ) ≥ d# ∈ A then
return true;
end
return false;
function badtypes(T ) : 2T
return {τ ∈ T |"∀R.C, d# ∈ τ and for all τ ! ∈ T : if "C, d! # ∈ τ ! then
max(1 − ∆R (τ, τ ! ), d! ) > d};
Algorithm 1: The Type Elimination-based Decision Procedure FixIt(ALC)
3.2 Soundness, Completeness and Termination
The termination, soundness, and completeness of our algorithm can be proven formally.
Theorem 1 (Termination). For any ALC knowledge base K = (T , A) the algorithm
FixIt(ALC) terminates after finitely many steps with either true or false as return
value.
Proof. The initialization step of the algorithm takes finitely many steps since the number
of K-types is finite. The repeat-loop must terminate after finitely many steps, since we
start with a finite set of types T in the beginning: if we do not remove any type in an
iteration (i.e. badtypes(T ! ) = ∅) we have T = T ! at the end of the loop (i.e. reaching
a fixpoint) and therefore terminate the loop. On the other hand, if badtypes(T ! ) 4= ∅ in
an iteration, at least one type is removed from T ! and hence T ⊂ T ! . This means, that
the input set of types T for the next iteration is finite and strictly smaller. Clearly, the
empty set is a fixpoint of badtypes(·) too, i.e. badtypes(∅) = ∅. Hence, we can repeat
the loop only finitely many times until we finally will reach a fixpoint. Since this fixpoint
T is a subset of the finite set of the initial set of types and there are only finitely many
possible mappings π to consider, deciding the criterion in the if-statement (based on T )
takes as well only finitely many steps. Therefore, the algorithm terminates with one of
the return-statements that give as a result either true or false.
The following lemma is a key element of the soundness and completeness proof and
shows that by successively removing bad types we can indeed ensure that types encode
possibility degree assignments to concepts that coincide with the canonical interpreta-
tion, and that any such canonical interpretation is a model of the T .
Let T be the set of types that is computed as the fixpoint in the algorithm FixIt(ALC),
i.e. badtypes(T ) = ∅ and let IT = (T, ·IT ) be a canonical interpretation for T as defined
above.
Lemma 1. For each K-type τ , concept C ∈ cl(K) and d ∈ PossDeg(K) it holds that
C IT (τ ) = d iff. *C, d+ ∈ τ . Further, IT |= T .
Proof. For the first part of the lemma, let τ be any K-type and d ∈ PossDeg(K) be any
relevant possibility degree.
We show by induction over the structure of concepts C ∈ cl(K) that *C, d+ ∈ τ
iff. C IT (τ ) = d: the base case (i.e. C ∈ cl(K) is an atomic concept name C ∈ C or
C = ") is trivially satisfied by our definition of IT . For the induction step, we consider
the different cases of compound concept expressions C ∈ cl(K) one-by-one:
1. for C = C1 # C2 ∈ cl(K), we know that C1 , C2 ∈ cl(K). By clause (3) in
our definition of types, we know that *C, d+ = *C1 # C2 , d+ ∈ τ iff. *C1 , d1 + ∈ τ and
*C2 , d2 + ∈ τ and d = min(d1 , d2 ). Applying the induction hypothesis to C1 and C2 , we
know that this is the case iff. C1 IT (τ ) = d1 and C2 IT (τ ) = d2 and d = min(d1 , d2 )
iff. d = min(C1 IT (τ ), C2 IT (τ )) iff. d = (C1 # C2 )IT = C IT by the by the semantics
of # in ALC.
2. for C = C1 $ C2 ∈ cl(K) the proof is analogous.
3. for C = ¬D ∈ cl(K), we know that D ∈ cl(K) by the definition of cl(K).
Because of clause (2) and the maximality requirement in our definition of K-types, we
know that *C, d+ = *¬D, d+ ∈ τ iff. *D, 1 − d+ ∈ τ . Applying the induction hypothesis
I
for D, we know that this holds iff. DIT (τ ) = 1 − d iff. (¬D) T (τ ) = C IT (τ ) = d by
the semantics of concept negation in ALC.
4. for C = ∀R.D ∈ cl(K), D ∈ sub(K) holds and hence D ∈ cl(K) by the
definition of cl(K).
First, we show one direction, i.e. that C IT (τ ) = d if *C, d+ ∈ τ : Assume that
*C, d+ = *∀R.D, d+ ∈ τ . According to the semantics of the universal role restriction in
I
ALC and our definition of IT , we have C IT (τ ) = (∀R.D) T (τ ) = inf τ ! ∈T {max(1 −
RIT (τ, τ ! ), DIT (τ ! ))} = inf τ ! ∈T {max(1 − ∆R (τ, τ ! ), DIT (τ ! ))}. We show that d is
a lower bound for {max(1 − ∆R (τ, τ ! ), DIT (τ ! ))|τ ! ∈ T }: Assume there exists a τ ! ∈
T s.t. d > max(1 − ∆R (τ, τ ! ), DIT (τ ! )). Let DIT (τ ! ) = d! . Applying the induction
hypothesis to D ∈ cl(K), we know *D, d! + ∈ τ ! . Hence, both d > 1 − ∆R (τ, τ ! )
and d > d! must hold. Hence ∆R (τ, τ ! ) > 1 − d. But, since *∀R.D, d+ ∈ τ this is
not possible by our by our definition of ∆R , because ∆R (τ, τ ! ) ≤ 1 − d. From the
contradiction we can conclude that d is in fact a lower bound for the considered set.
Therefore, d ≤ inf τ ! ∈T {max(1 − ∆R (τ, τ ! ), DIT (τ ! ))}
Next, we show that inf τ ! ∈T {max(1 − ∆R (τ, τ ! ), DIT (τ ! ))} ≤ d too, by proving
that there exists a τ ! ∈ T s.t. max(1 − ∆R (τ, τ ! ), DIT (τ ! )) ≤ d. Assume, the contrary,
i.e. for all τ ! ∈ T : max(1 − ∆R (τ, τ ! ), DIT (τ ! )) > d (‡). By applying our induction
hypothesis to D and τ ! , we know that this is the case iff. for all τ ! ∈ T : if *D, d! + ∈ τ !
then max(1 − ∆R (τ, τ ! ), d! ) > d. But then, τ would be a bad type which contradicts
the fact that T the computed fixpoint which can not contain any bad types (i.e. τ ∈
badtypes(T ) = ∅). Hence our assumption (‡) must be wrong, and we can conclude
that inf τ ! ∈T {max(1 − ∆R (τ, τ ! ), DIT (τ ! ))} ≤ d. Therefore, d = inf τ ! ∈T {max(1 −
∆R (τ, τ ! ), DIT (τ ! ))}, and hence d = C IT (τ ).
The other direction of the induction hypothesis (i.e. that *∀R.D, d+ ∈ τ if (∀R.D)IT (τ ) =
d) can now be proven as follows: Assume that (∀R.D)IT (τ ) = d (†) but *∀R.D, d+ 4∈ τ .
By the maximality requirement in our definition of K-types there must hence exist a
d! ∈ PossDeg(K) s.t. *∀R.D, d! + ∈ τ and d! 4= d. Using the same argument as for the
if-direction in this case, we can therefore conclude that (∀R.D)IT (τ ) = d! 4= d which
contradicts (†). Hence, our assumption must be wrong and *∀R.D, d+ ∈ τ must hold
whenever (∀R.D)IT (τ ) = d.
For the second part of the lemma, to show that IT |= T , assume that for some
α = C ) C ! ∈ T and some τ ∈ T it holds that C IT (τ ) > C !IT (τ ), in other words,
if C IT (τ ) = d and C !IT (τ ) = d! then d > d! . Thus, we can deduce (from the first
part of this lemma) that, if *C, d+ ∈ τ and *C ! , d! + ∈ τ then d > d! . However, by our
definition of K-type (i.e. clause (5)), we also know that in this case d ≤ d! must hold,
which is contradictive. Hence, our assumption must be wrong and IT |= α for each
α ∈ T which means that IT |= T .
Theorem 2 (Soundness). If FixIt(ALC) returns true for a ALC knowledge base K =
(T , A), then K is satisfiable.
Proof. We show that a canonical interpretation IT for the computed fixpoint T can be
extended to a model of K. By Lemma 1, we already know that IT |= T . We now show,
that IT can be extended such that IT |= A too, which completes the proof: Since the
algorithm returns true, there exist a total function π : IndA → T s.t. *C, d! + ∈ π(o)
and d ≤ d! for each *o : C ≥ d+ ∈ A ()), and ∆R (π(o), π(o! )) ≥ d for each
*R(o, o! ) ≥ d+ ∈ A (†). We extend the definition of IT to the ABox A as follows: for
all Abox individual names o ∈ IndA , we set oIT := π(o) ∈ T . First, consider an
ABox axiom of the form α = *o : C ≥ d+ ∈ A. Then, IT |= α iff. C IT (oIT ) ≥ d,
iff. C IT (π(o)) ≥ d iff. there exists a d! ≥ d s.t. C IT (π(o)) = d! . By Lemma 1 this is
the case iff. there exists a d! ≥ d s.t. *C, d! + ∈ π(o) which is satisfied since ()) holds.
Second, consider an ABox axiom of the form α = *R(o, o! ) ≥ d+ ∈ A. Then, IT |= α
I
iff. RIT (oIT , o! T ) ≥ d iff. ∆R (π(o), π(o! )) ≥ d (by Def. of the extended IT ). The
latter is satisfied because of (†).
An second key element for the completeness proof is the following lemma that
shows that our canonical way of interconnecting types (in the fixpoint set) is maximal
or the strongest possible one in the following sense: the interconnection R of individuals
o, o! defined by any model I of K is covered by the canonical interconnection ∆R of
the respective types τ (o), τ (o! ) representing o, o! in I.
Lemma 2. Let I = (∆I , ·I ) be any model of K = (T , A). For each individual o ∈ ∆I
we define its corresponding type τ (o) := {*C, d+ ∈ cl(K) × PossDeg(K)|C I (o) = d}.
Then, ∆R (τ (o), τ (o! )) ≥ RI (o, o! ) for all o, o! ∈ ∆I .
Proof. Assume that there exist o, o! ∈ ∆I s.t. ∆R (τ (o), τ (o! )) < RI (o, o! ). By our
definition of ∆R , we then know that δ(d, d! ) < RI (o, o! ) (∗) for some *∀R.C, d+ ∈ τ (o)
and *C, d! + ∈ τ (o! ). From the definition of τ (·), we know that δ(d, d! ) < RI (o, o! ) for
some o, o! ∈ ∆I s.t. (∀R.C)I (o) = d and C I (o! ) = d! . From the semantics of ∀R.C in
ALC, we derive d = inf o!! ∈∆I {max(1 − RI (o, o!! ), C IT (o!! ))}. Hence, in particular
d ≤ max(1 − RI (o, o! ), C IT (o! )) = max(1 − RI (o, o! ), d! ) (†). We consider two
cases: first, d! < d, then in order to satisfy (†), max(1 − RI (o, o! ), d! ) = 1 − RI (o, o! )
must hold and (†) simplifies to d ≤ 1−RI (o, o! ) iff. RI (o, o! ) ≤ 1−d. Since d! < d, (∗)
simplifies to 1−d < RI (o, o! ), hence, 1−d < RI (o, o! ) ≤ 1−d which is contradictory.
In the second case, we assume that d! ≥ d. Hence, δ(d, d! ) = 1. Then, (†) simplifies
to 1 < RI (o, o! ), which is contradictory, since RI (o, o! ) ∈ PossDeg(K) and 1 is
the maximum possibility degree in PossDeg(K). Therefore, in both cases we reach a
contradiction and can conclude that our assumption must be wrong. This concludes the
proof.
Theorem 3 (Completeness). If an ALC knowledge base K = (T , A) is satisfiable,
then FixIt(ALC) returns true for K
Proof. Let I = (∆I , ·I ) be any model of K = (T , A), i.e. I |= T and I |= A.
In [13,14] it is shown that a KB in ALC is consistent iff. there is a model I of the
KB which only assigns possibility degrees that occur in the ABox A for interpreting
atomic concept or role names. Hence, without loss of generality, we can assume in the
following that I assigns possibility degrees in PossDeg(K) only.
For each individual o ∈ ∆I we define its corresponding type τ (o) := {*C, d+ ∈
cl(K) × PossDeg(K)|C I (o) = d} and define TI := {τ (o)|o ∈ ∆I }. It is easy to see
that TI is a set of K-types. Further, TI 4= ∅ since ∆I 4= ∅.
Let T (i) denote the set of types that is computed after i iterations of the repeat-loop
in our algorithm. We first show that TI ⊆ T (i) for all i ≥ 0 by induction over the
number of iterations i:
In the base case i = 0, our initialization step sets T (0) to contain all K-types. Since
TI consists of K-types only, TI ⊆ T (0) must hold. To proof the induction step, we
assume that TI ⊆ T (i) but TI 4⊆ T (i+1) . Therefore, there must be a τ (o) ∈ TI s.t.
τ (o) ∈ T (i) but not τ (o) ∈ T (i+1) . From the repeat-loop in the algorithm, we know
that T (i+1) = T (i) badtypes(T (i) ). Consequently, τ (o) must be a bad type τ (o) ∈
badtypes(T (i) ) and we can not have reached a fix-point yet.
From our definition of bad-types we can derive that there must exist a *∀R.C, d+ ∈
τ (o) and for all τ ! ∈ T (i) : if *C, d! + ∈ τ ! then max(1 − ∆R (τ, τ ! ), d! ) > d} (‡). Since
TI ⊆ T (i) (‡) must hold in particular for all τ (o! ) ∈ TI . Using our definition of τ (·)
we can rephrase (‡) as follows: there must exist a ∀R.C ∈ cl(K) s.t. for all o! ∈ ∆I :
max(1 − ∆R (τ (o), τ (o! )), C I (o! )) > (∀R.C)I (o) ()).
By Lemma 2, we know that ∆R (τ (o), τ (o! )) ≥ RI (o, o! ) for all o, o! ∈ ∆I . Hence,
1 − ∆R (τ (o), τ (o! )) ≤ 1 − RI (o, o! ) (∗) for all o, o! ∈ ∆I . Since max(a, b) ≤
max(a! , b) for any a, a! , b s.t. a ≤ a! , we can reformulate ()) using (∗) as follows:
there must exist a ∀R.C ∈ cl(K) s.t. for all o! ∈ ∆I : max(1 − RI (o, o! ), C I (o! )) >
(∀R.C)I (o)} (*), which contradicts the fact that (∀R.C)I (o) = inf o! ∈∆I {max(1 −
RI (o, o! ), C I (o! ))}: Since RI (o, o! ) ∈ PossDeg(K) and C I (o! ) ∈ PossDeg(K), we
know that max(1 − RI (o, o! ), C I (o! )) ∈ PossDeg(K) for all o! ∈ ∆I by our def-
inition of PossDeg(K). Because ∆I 4= ∅ and PossDeg(K) is a finite set, there must
exist an o∗ ∈ ∆I for which max(1 − RI (o, o∗ ), C I (o∗ )) is minimal, i.e. max(1 −
RI (o, o∗ ), C I (o∗ )) ≤ max(1 − RI (o, o! ), C I (o! )) for all o! ∈ ∆I . Hence, d∗ :=
max(1 − RI (o, o∗ ), C I (o∗ )) ∈ PossDeg(K) is a lower bound for the set {max(1 −
RI (o, o! ), C I (o! )|o! ∈ ∆I }. However, from (*) we know that d < d∗ , hence d can not
be the greatest lower bound (i.e. the infimum) of the set {max(1−RI (o, o! ), C I (o! )|o! ∈
∆I }, hence ∀R.C)I (o) = d∗ > d which is contradictive.
Therefore, our assumption that τ (o) is a bad type must be wrong and we have com-
pleted the proof of the induction step as well as the induction argument.
We continue the proof of the lemma as follows: since T = T (i) is the fixpoint that
is computed in the loop in our algorithm in i steps for some i ≥ 0, we know that
TI ⊆ T (i) = T . Consider the mapping πI : IndA → T defined by πI (o) := τ (oI ) for
all o ∈ IndA . Then, πI is a well-defined, total function from IndA to T . We now show
that this specific mapping πI satisfies the condition that is checked in the if-statement
of the algorithm:
In the first case, we consider any Abox axiom α ∈ A of the form α = *o : C ≥ d+.
Since I |= A, I |= α must hold. I |= α iff. C I (oI ) ≥ d iff. C I (oI ) = d! for some
d! ∈ PossDeg(K) with d! ≥ d iff. *C, d+ ∈ τ (oI ) for some d! ∈ PossDeg(K) with
d! ≥ d (by Lemma 1) iff. *C, d+ ∈ πI (o) for some d! ∈ PossDeg(K) with d! ≥ d
(by our definition of πI ). Hence, the respective part of the if-condition for α holds
for πI . In the second case, we consider any Abox axiom α ∈ A of the form α =
*R(o, o! ) ≥ d+. Since, I |= A, I |= α must hold. I |= α holds iff. RI (oI , o!I ) ≥ d.
Since ∆R (τ (o), τ (o! )) ≥ RI (oI , o!I ) by Lemma 2, we know that ∆R (τ (oI ), τ (o!I )) ≥
d and therefore ∆R (πI (o), πI (o)) ≥ d by our definition of πI . Hence, the respective
part of the if-condition for α is as well satisfied by πI . Consequently, the tested if-
condition is satisfied by πI and the algorithm returns true.
This leads to the main result, which is an immediate consequence of Theorems 2,
3, and 1:
Corollary 1. The algorithm FixIt(ALC) is a sound and complete decision procedure
for knowledge base satisfiability in ALC.
4 Related Work
Our method FixIt(ALC) generalizes the principle (i.e. a type elimination process) un-
derlying the top-down variant of the KBDD procedure proposed in [6] for the modal
logic K to the (more expressive) FDL ALC. Further, our method integrates (fuzzy)
ABoxes and TBoxes in the inference process both of which are not dealt with in KBDD.
So far, reasoning in Fuzzy DLs has been mostly based on tableau-methods (e.g., [13,12,4,11]).
Most of these methods do not support reasoning with general terminologies as it is pos-
sible with FixIt(ALC). The first method ever to integrate GCIs into FDL reasoning
is [12]. A very similar approach is presented in [4] for the fuzzy variant of a more ex-
pressive DL, namely SHI. Very recently, [16] proposed a novel and elegant method
for reasoning with GCIs (under a more general semantics than here) which is inspired
by earlier works on tableau-based reasoning in multi-valued logics. To the best of our
knowledge there is no other approach to deal with GCIs in FDLs available at present.
FixIt(ALC) therefore represents an interesting enrichment of inference calculi tool-
box for FDLs, since no non-determinism is introduced by considering GCIs. A similar
effect is achieved in [16] by the substantial modification of a standard tableau-based
method and an extension with an MILP oracle. A very similar approach to [16] that is
not fixed to a specific semantics is presented in [3].
Further, [14] demonstrates how to use inference procedures for classical DLs to perform
reasoning in (some) FDLs. This allows to use algorithms that have been developed for
classical DLs in FDL reasoning (for some FDLs) in an indirect way. Please note that the
KBDD procedure can not be used in such an indirect way to perform ALC reasoning,
since both TBoxes and ABoxes are not supported.
5 Conclusions and Future Work
We presented a novel procedure FixIt(ALC) for deciding knowledge base (KB) sat-
isfiability in the FDL ALC, introducing a new class of inference procedures into FDL
reasoning. Besides the tableau-based methods [12,4,16,3], it is the only (and the first
non-tableau-based) approach to integrate general terminologies in FDL reasoning that
we are aware of.
The main research questions that we want to address next are as follows: we will
study means of implicit representation of sets of fuzzy types known from Symbolic
Model Checking, in particular their implementation by means of Ordered Binary Deci-
sion Diagrams (OBDDs) similar to [6], therefore addressing the main obstacle to apply
the procedure in practice. A major question concerning optimization is clearly how to
implement the final test of the algorithm efficiently, e.g. by heuristic search using the
information in the ABox effectively to find the required mapping. The integration of
optimizations such as full vs. lean representations or particle vs. types as discussed
in [6] should be straightforward. We want to evaluate the effectiveness of the method
by an implementation and comparison to tableau-based systems for FDLs. Moreover,
we believe that it is interesting to study a bottom-up variant of KBDD in the context
of FDLs too, and to check if the integration of ABoxes can be done more efficiently
in such a variant. Finally, we would like to see to what extend the method can cover
other semantics for FDLs (e.g. other t-norms) and extended constructs, such as fuzzy
modifiers and concrete domains.
References
1. F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, and P. F. Patel-Schneider, editors.
The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge
University Press, 2003.
2. R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM
Comput. Surv., 24(3):293–318, 1992.
3. V. Haarslev, H. Pai, and N. Shiri. Uncertainty Reasoning for Ontologies with General TBoxes
in Description Logic. In P. C. G. Costa, C. D’Amato, N. Fanizzi, K. B. Laskey, K. Laskey,
T. Lukasiewicz, M. Nickles, and M. Pool, editors, Uncertainty Reasoning for the Semantic
Web I, LNAI. Springer, 2008.
4. Y. Li, B. Xu, J. Lu, and D. Kang. Discrete Tableau Algorithms for F SHI. In Proceedings
of the International Workshop on Description Logics (DL), 2006.
5. K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell, MA,
USA, 1993.
6. G. Pan, U. Sattler, and M. Y. Vardi. BDD-based decision procedures for the modal logic K.
Journal of Applied Non-Classical Logics, 16(1-2):169–208, 2006.
7. P. F. Patel-Schneider, P. Hayes, and I. Horrocks. OWL Web Ontology Language Semantics
and Abstract Syntax. Candidate Recommendation 18 August 2003, W3C, 2003.
8. V. R. Pratt. A Near-Optimal Method for Reasoning about Action. J. Comput. Syst. Sci.,
20(2):231–254, 1980.
9. K. Schild. A correspondence theory for terminological logics: Preliminary report. In In
Proceedings of the International Joint Conference of Artificial Intelligence (IJCAI 1991),
pages 466–471, 1991.
10. M. Schmidt-Schauß and G. Smolka. Attributive Concept Descriptions with Complements.
Artif. Intell., 48(1):1–26, 1991.
11. G. Stoilos, G. B. Stamou, J. Z. Pan, V. Tzouvaras, and I. Horrocks. Reasoning with very
expressive fuzzy description logics. J. Artif. Intell. Res. (JAIR), 30:273–320, 2007.
12. G. Stoilos, U. Straccia, G. Stamou, and J. Pan. General Concept Inclusions in Fuzzy De-
scription Logics. In Proceedings of the 17th Eureopean Conference on Artificial Intelligence
(ECAI-06), pages 457–461. IOS Press, 2006.
13. U. Straccia. Reasoning within Fuzzy Description Logics. Journal of Artificial Intelligence
Research, 14:137–166, 2001.
14. U. Straccia. Transforming Fuzzy Description Logics into Classical Description Logics. In
Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA-04),
number 3229 in Lecture Notes in Computer Science, pages 385–399, Lisbon, Portugal, 2004.
Springer Verlag.
15. 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.
16. U. Straccia and F. Bobillo. Mixed integer programming, general concept inclusions and
fuzzy description logics. Mathware & Soft Computing, 14(3):247–259, 2007.