corresponding to L 1 and L 2 are built over disjoint sets of function symbols. For the DLs introduced in Section 2, this can be achieved by assuming that the sets of role names of L 1 and L 2 are disjoint and the sets of nominals of L 1 and L 2 are disjoint. The DL L 1 & L 2 then allows the use of the concept and role constructors of both DLs, but in a restricted way.

Role descriptions are either role descriptions of L 1 or of L 2 . There are no role descriptions involving constructors or names of both DLs. Concept descriptions may contain concept constructors of both DLs; however, a constructor of Li may only use a role description of Li (i = 1, 2).

Let us illustrate these restrictions by two simple examples. The fusion ALC+ ® ALC- 1 of the two DLs ALC+ and ALC- 1 is the fragment of ALC+ ,- 1 whose set of role names is partitioned into two sets NR, and NR, such that
- the transitive closure operator may only be applied to names from N R 1 ;
- the inverse operator may only be applied to names from N R , .

For example, if A is a concept name, R E N R, and Q E N R,, then BR+.A n VQ-1.-A is a concept description of ALC+ ® ALC- 1 , but ¬ R+.A n ¬ R¬ ¬ ¬ A and ¬ (Q¬ 1 )+.A are not.

Note that, although the two source DLs have disjoint sets of role names, in ALC+ ® ALC- 1 role names from both sets may be used inside existential and value restrictions since these concept constructors are available in both DLs.

The fusion ALCQ ® ALC R + of the two DLs ALCQ and ALC R + is the fragment of ALCQR+ whose set of role names NR (with transitive roles NR+ C NR) is partitioned into two sets NR, and NR, with NR+ C NR, such that, inside qualifying number restrictions, only role names from NR, may be used. In particular, this means that transitive roles cannot occur within qualified number restrictions.

In the following, we give examples that illustrate the usefulness of the transfer results proved in the previous section.  First, we will give an example for the case of satisfiability and then for relativized satisfiability. Subsequently, we will consider a more complex example involving so-called concrete domains. Here, our general transfer result can be used to prove a decidability result that has only recently been proved by designing a specialized algorithm for the fusion. Finally, we will give an example that demonstrates that the restriction to local ADSs is really necessary.

## 5.1 Decidability Transfer For Satisfiability

In this subsection, we will give an example for an application of Theorem 29 where the decidability result could not be obtained using Theorem 17.

Theorem 29 requires the ADSs to have covering normal terms. This is, however, satisfied by all the DLs that yield local ADSs.

Proposition 35. Let L be one of the DLs introduced in Section 2, and let the corresponding ADS S = (L,M) be local.  Then S has covering normal terms, and these terms can be computed in linear time. Proof.  For all function symbols f in L , the term t f has the form f vR ( x ) for some role description R . The semantics of value restrictions implies that terms of this form satisfy