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.