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 necessarily 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 introducing a new class of inference procedures into FDL reasoning.
Description Logics (DLs) [
So far, reasoning in Fuzzy DLs is mainly based on tableau-methods (e.g. [
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. [
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 [
Our method is interesting especially regarding the last aspect since the handling of
general terminologies in standard tableau-based methods (e.g. [
We introduce ALC [
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
expressions 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
interrelations: a (fuzzy) ABox axiom is either a *i : C "# d+ or a *R(i, i!) ≥ d+ s.t. i, i! ∈ I,
d ∈ [
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
nonempty set ΔI called the domain, and a function ·I which maps each concept name
C ∈ C to a fuzzy set CI : ΔI → [
An interpretation I satisfies a TBox axiom α = C ) D iff. for all o ∈ ΔI it holds that CI (o) ≤ DI (o), i.e. C is a fuzzy subset of D. I satisfies an ABox axiom α = *i : C "# d+ iff. CI (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 CI (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 CI (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 CI (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 ∈ [
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
satisfiability wrt. a TBox, entailment of fuzzy ABox assertions, or the BTVB problem) can
be reduced to KB satisfiability checking (cnf. [
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 constructs 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 derive a model for the given knowledge base K iff. K is satisfiable. In contrast to tableaubased 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+ [
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 [
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 interpretations for K. More specifically, the notion of a type allows to represent individuals 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 canonical) 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 CIT (τ ) = 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 terminology T , i.e. it satisfies that
CIT (τ ) = 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 CIT (τ ) ≥ 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 (τ, τ !), CIT (τ !)) | τ ! ∈ T }
Types τ in which the possibility degree assigned d to ∀R.C is too small to be consistent 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 elimination 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 interpretation. 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 interpretation, 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 CIT (τ ) = 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. CIT (τ ) = 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. C1IT (τ ) = d1 and C2IT (τ ) = d2 and d = min(d1, d2) iff. d = min(C1IT (τ ), C2IT (τ )) iff. d = (C1 # C2)IT = CIT 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 for D, we know that this holds iff. DIT (τ ) = 1 − d iff. (¬D)IT (τ ) = CIT (τ ) = 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 CIT (τ ) = d if *C, d+ ∈ τ : Assume that *C, d+ = *∀R.D, d+ ∈ τ . According to the semantics of the universal role restriction in ALC and our definition of IT , we have CIT (τ ) = (∀R.D)IT (τ ) = 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 = CIT (τ ).
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 CIT (τ ) > C!IT (τ ), in other words, if CIT (τ ) = 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. CIT (oIT ) ≥ d, iff. CIT (π(o)) ≥ d iff. there exists a d! ≥ d s.t. CIT (π(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 |= α iff. RIT (oIT , o!IT ) ≥ 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)|CI (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 CI (o!) = d!. From the semantics of ∀R.C in ALC, we derive d = inf o!!∈ΔI {max(1 − RI (o, o!!), CIT (o!!))}. Hence, in particular d ≤ max(1 − RI (o, o!), CIT (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 [
For each individual o ∈ ΔI we define its corresponding type τ (o) := {*C, d+ ∈ cl(K) × PossDeg(K)|CI (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!)), CI (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!), CI (o!)) > (∀R.C)I (o)} (*), which contradicts the fact that (∀R.C)I (o) = inf o!∈ΔI {max(1 − RI (o, o!), CI (o!))}: Since RI (o, o!) ∈ PossDeg(K) and CI (o!) ∈ PossDeg(K), we know that max(1 − RI (o, o!), CI (o!)) ∈ PossDeg(K) for all o! ∈ ΔI by our definition 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∗), CI (o∗)) is minimal, i.e. max(1 − RI (o, o∗), CI (o∗)) ≤ max(1 − RI (o, o!), CI (o!)) for all o! ∈ ΔI . Hence, d∗ := max(1 − RI (o, o∗), CI (o∗)) ∈ PossDeg(K) is a lower bound for the set {max(1 − RI (o, o!), CI (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!), CI (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 completed 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. CI (oI ) ≥ d iff. CI (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 ifcondition 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
Our method FixIt(ALC) generalizes the principle (i.e. a type elimination process)
underlying the top-down variant of the KBDD procedure proposed in [
Further, [
We presented a novel procedure FixIt(ALC) for deciding knowledge base (KB)
satisfiability in the FDL ALC, introducing a new class of inference procedures into FDL
reasoning. Besides the tableau-based methods [
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
Decision Diagrams (OBDDs) similar to [