Proof: **We give the proof of the first item. The second one is proved analogously but using the second item in Lemma 4.2.**
Let us assume that K = hA, T i **is an unfoldable fuzzy KB. We know that all**
axioms in T are either of the form hA ⊑ C ≥ 1i or A ≡ C, where A **is an atomic** concept. The algorithm consists on two steps. In the first step, we replace all axioms of the form hA ⊑ C ≥ 1i with A ≡ A′ ⊓ C (with A′ **a new atomic** concept). Once this is done we know that all axioms in the new TBox K′ **are of**
the form A ≡ C**. In the second step of the algorithm, we consider the ABox** A and replace, for every axiom A ≡ C, all occurrences of A with C**. We will refer**
by A⋆**to the output of this process.**
Now let us check that K is satisfiable iff A⋆**is satisfiable. The first item in**
Lemma 4.2 takes care of the first step of the algorithm, that is, K **is satisfiable**
iff K′is satisfiable. Next we prove that K′is satisfiable iff A⋆**is satisfiable.**
The rightwards direction is trivial. For the other, it is enough to notice that since the axioms in K′ are of the form A ≡ C with A **an atomic concept we can**
redefine, for every individual a **appearing in the ABox** A⋆, AI(a I**) as the value**
C
I(a I). **Q.E.D.**
Next theorem is formulated only for Lukasiewicz in order to use the **decidability result in [12, Corollary 1] for our framework. We include t-conorm as a**
concept constructor as opposed to [12], but Lukasiewicz t-conorm is clearly definable from Lukasiewicz t-norm and negation. Extensions of [12, Corollary 1]
adding a t-norm constructor would be needed in order to deal with all t-norm logics considered in this paper, and not only Lukasiewicz.

## Theorem 4.4 ( Lukasiewicz Case)

1. For every fuzzy KB K = hA, T i such that T **is acyclic, the satisfiability in**
a finite model under the fuzzy ALC **coincides with the satisfiability.**
2. There is an algorithm for checking the satisfiability of acyclic KBs.

Proof: **By Lemma 4.1 and Lemma 4.3 it is possible to remove the TBox.**
Then, we use the known results [12, Theorem 8 and Corollary 1] that **in fuzzy**
ALC **ABoxes, satisfiability in a witnessed model and satisfiability in a finite**
model coincide and are decidable problems. Note that [12] does not consider a t-conorm in the language, but it can defined from Lukasiewicz negation and t-norm. The proof finishes using the result in [13] which tells **us that**
for Lukasiewicz, satisfiability coincides with satisfiability in a witnessed model. Q.E.D.

On the other hand, the second remark concerns the fact there are several reasoning algorithms in the literature for Lukasiewicz [7, 21, 22], Product [6], or any left continuous t-norm fuzzy DLs [8, 18]) that claim to support GCIs. These algorithms restrict themselves to witnessed models. Unfortunately, these papers are implicitly assuming that the logic satisfies FMP. By Theorems 3.3 and 3.7 we have shown that this assumption cannot be done, so these algorithms do not work correctly for arbitrary fuzzy KBs (even if the semantics of GCIs is defined using Zadeh's set inclusion, as it happens in [18]). For instance,