with hC ⊓ α ⊑ D ≥ 1i**. Next, we exploit a similar idea to show that, in the**
particular case of Lukasiewicz, unfoldable fuzzy TBoxes can be converted into acyclic ones, even without having truth constants α **as concept constructors.** The idea is that all axioms of the form hA ⊑ C ≥ αi **can be converted into the** form hA ⊑ C
′ ≥ 1i**. For example,** hA ⊑ C ≥
2 3 i **can be converted into the form**
hA ⊑ C ⊔ ((A′ ⊓ A′) ⊓ ¬(A′ ⊓ A′ ⊓ A′)) ≥ 1i ,
where A′**is a new atomic concept; the reason why this is so is because the** concept (A′ ⊓ A′) ⊓ ¬(A′ ⊓ A′ ⊓ A′**) always takes values onto the interval [0**,
1 3
].

In the following proof we develop this idea.

Lemma 4.1 ( Lukasiewicz Case) **There is an algorithm that converts every**
acyclic fuzzy KB K = hA, T i **into an unfoldable fuzzy KB** K′ = hA, T
′i **in such**
a way that K is satisfiable iff K′**is satisfiable.**
The algorithm also preserves satisfiability in a witnessed model, and the same for satisfiability in a finite model.

Proof: Let us consider an axiom of the form hA ⊑ C ≥ αi**. By the constructive version of McNaughton's Theorem (see [1]) it is obvious that there is an**
algorithm that for every rational α **generates a propositional concept** τα(A′)
using only one atomic concept A′ **and such that**
P1: τα(A′**) only takes values in [0**, 1 − α], P2: τα(A′) takes value 1 − α when A′**takes value** α.

To finish the proof it is enough to see that for every KB K**, it holds that**
- K ∪ {hA ⊑ C ≥ αi} **is satisfiable, iff**
- K ∪ {hA ⊑ C ⊔ τα(A′) ≥ 1i} is satisfiable (where A′**is a new atomic concept).**
The upwards implication is a consequence of P1. On the other hand, the downwards implication is a consequence of P2 because we can extend any interpretation I to encompass the new atomic concept A′ **defining for every individual**
x, A′I(x) = α. It is also obvious that this way of extending the interpretation preserves the witnessed property (because A′**takes the same value in all**
individuals) and the finiteness. **Q.E.D.**
Next we prove, using ideas from [19], that fuzzy unfoldable TBoxes can be eliminated through a finite expansion process when the interpretation of ⊓ is a continuous t-norm. Our proof of this result does not seem to work for satisfiability in a witnessed model; but we know how to deal with this case as long as the minimum constructor min{C, D} **is definable in our framework.** We remind the reader that in the case of continuous t-norms the constructor min{C, D} is definable, using an R-implication constructor →**, by** C ⊓(C → D);