C ¹ΣT D can be reduced to the case of an empty terminology by applying the KB **expansion**
process. So, without loss of generality, we can limit our attention to the **case** C ¹∅ D.

At first, an analogue to relation (12) holds. In fact, it can easily be shown **that**
Proposition 5 Let C and D be two concepts. It follows that C ¹∅ D iff for all n > 0 ha:C ≥ ni|≈ha:D ≥ ni, where a is a new **individual.** ⊣
Proof:

```
 ⇒ .) Assume that C ¹∅ D holds. Suppose to the contrary that ∃n > 0 such that
ha:C ≥ ni 6|≈ha:D ≥ ni. Therefore, there is an interpretation I and an n > 0 such that
C
I(a
  I
  ) ≥ n and DI(a
           I
           ) < n. But, from the hypothesis n ≤ C
                              I
                              (a
                                I
                                ) ≤ DI(a
                                     I
                                     ) < n follows.
Absurd.
    
 ⇐ .) Assume that for all n > 0, ha:C ≥ ni|≈ha:D ≥ ni holds. Suppose to the contrary
that C 6¹∅ D holds. Therefore, there is an interpretation I and d ∈ ∆Isuch that C
                                         I
                                         (d) >
DI(d) ≥ 0. Let us extent I to a such that a
                      I = d and consider n = C
                                  I
                                  (d) > 0. Of course,
I satisfies ha:C ≥ ni. Therefore, from the hypothesis it follows that I satisfies ha:D ≥ ni,
i.e. DI(d) ≥ n = C
         I
         (d) > DI(d). Absurd. ✷
How can we check whether for all n > 0 ha:C ≥ ni|≈ha:D ≥ ni holds? A solution to this
problem, restricted to the propositional case, is given by Straccia (2000a). Indeed, it is
shown that

```

Proposition 6 (Straccia, 2000a) Let p and q be two propositions, 0 < n1 ≤ 0.5 and 1 ≥ n2 > 0.5. It follows that for all n > 0, hp ≥ ni|≈hq ≥ ni iff for **both** m ∈ {n1, n2},
hp ≥ mi|≈hq ≥ mi **holds.** ⊣
The above proposition establishes that, at the propositional level, in order to check **whether**
hp ≥ ni|≈hq ≥ ni holds for all n, it is sufficient to check the entailment relation with **respect**
to two values n1, n2. The first being less or equal than 0.5, while the second being **greater**
than 0.5, respectively. This is due to the fact that for given **values** n, n
′ ≤ 0.5, any **proof** of hp ≥ ni|≈hq ≥ ni can be converted into a proof for hp ≥ n
′
**i|≈h**q ≥ n
′
i and vice-versa. The case **where** n, n
′ > 0.5 is **similar.**
The above proposition can be extended to our fuzzy DL as **well.**

```
Lemma 1 Let C and D be two concepts, 0 < n, n
                              ′ ≤ 0.5 and let a be an individual. It
follows that ha:C ≥ ni|≈ha:D ≥ ni iff ha:C ≥ n
                           ′
                           i|≈ha:D ≥ n
                                   ′
                                   i. ⊣

```

Proof: It is enough to show that S = {ha:C ≥ ni,ha:D < ni} is satisfiable iff S
′ =

```
{ha:C ≥ n
           ′
           i,ha:D < n
                         ′
                         i} is satisfiable.
  ⇒ .) Assume that S is satisfiable. So, there is a clash-free completion S˜ of S. With
S˜[n/n
       ′
       ] we indicate the set of fuzzy constraints obtained from S˜, by replacing any value n
in S˜ with n
          ′ and any value 1 − n in S˜ with 1 − n
                                                        ′
                                                        
                                                          , respectively. We will show that S˜[n/n
                                                                                                      ′
                                                                                                      ]
is a clash-free completion of S
                                  ′ and, thus, S
                                                  ′
                                                  is satisfiable.
    Let r1, . . . , rk, k ≥ 0 be the sequence of inference rule applications, which applied to S
get S˜. Let S˜0 = S, let S˜k = S˜ and for 1 ≤ i ≤ k let S˜i be the set of fuzzy constraints
obtained from S˜i−1 by the application of the ri rule to S˜i−1.
    By induction on k, we show that (i) the sequence of inference rules r1, . . . , rk can be
applied to S
              ′ as well; (ii) for S˜′0 = S
                                         ′
                                         
                                          , S˜′k = S˜′ and S˜′i the set of fuzzy constraints obtained

```
