to our more general situation since it strongly depends on the normality of the modal operators.

Using Proposition 24, we obtain the following corollary to our first transfer theorem.

Corollary 25. Let S 1 , S 2 be local ADSs and assume that, for i E {1,2}, the relativized
(term) satisfiability problem for Si is decidable. Then the relativized (term) satisfiability problem for Si ® Si is decidable.

Proof.  We know by Theorem 17 (Corollary 22) that the relativized (term) satisfiability problem for S 1 ® S 2 is decidable. Hence, Proposition 24 yields that the relativized (term)
stisfiability problem for ( S 1 & S 2 ) V is decidable. But S V ® S V is just a notational variant of ( S 1    S 2 ) U : the function symbols f 3 U S , and f 3 U S , can be replaced by f 3 U S 1 analogously for fvus 1 ®s 2 ) since all three have identical semantics.

o

## 4.2 Satisfiability

Note that Theorem 17 does not yield a transfer result for the unrelativized satisfiability problem. Of course, if the relativized satisfiability problems for S 1 and S 2 are decidable, then the theorem implies that the satisfiability problem for S 1 ® S 2 is also decidable (since it is a special case of the relativized satisfiability problem). However, to be able to apply the theorem to obtain decidability of the satisfiability problem in the fusion, the component ADSs must satisfy the stronger requirement that the relativized satisfiability problem is decidable. Indeed, the set Γ i in Theorem 20 contains a term assertion (namely Τ Σ sur i ( V D )) en if Γ does not contain any term assertions.

There are cases where the relativized satisfiability problem is undecidable whereas the ssse the fusion of ALCF and ALC+,°,µ since the relativized satisfiability problem for ALCF is aready undecidable (Baader et al., 1993). However, the satisfiability problem is decidable for both DLs.

## 4.2.1 Covering Normal Terms

Before we can formulate a transfer result for the satisfiability problem, we need to introduce an additional notion, which generalizes the notion of a normal modal logic.

Definition 26 (Covering normal terms). Let ( L, M ) be an ADS and f be a function symbol of L of arity n. The term t f ( x ) (with one variable x ) is a covering normal term for f iff the following holds for all W E M:
- t 2 ( W ) = W
- for all X, Y ⊆ W, t Ψ ( X ∩ Y ) = t Ψ ( X ) ∩ t Ψ ( Y ), and
- for all X, X 1 , . . , Y n ⊆ W : X ∩ X i  = X ∩ Y i for 1 ≤ i ≤ n implies

$t_{f}^{\mathfrak{M}}(X)\cap f^{\mathfrak{M}}(X_{1},\ldots,X_{n})=t_{f}^{\mathfrak{M}}(X)\cap f^{\mathfrak{M}}(Y_{1},\ldots,Y_{n})$.  
An ADS ( L , M ) is said to have covering normal terms iff one can effectively determine a covering normal term t for every function symbol f of L .