
## 4. Fusions Of Abstract Description Systems

In this section, we define the fusion of abstract description systems and prove two transfer theorems for decidability, one concerning satisfiability and the other one concerning relativized satisfiability.

Definition 16. The fusion S 1 ® S 2 = ( L 1 ® L 2 , M 1 ® M 2 ) of two abstract description systems S 1 = ( L 1 , M 1 ) and S 2 = ( L 2 , M 2 ) over
- disjoint sets of function symbols F of L 1 and G of L 2 1
- disjoint sets of relation symbols R of L 1 and Q of L 2 , and
- the same sets of set and object variables is defined as follows: L 1 8 L 2 is the ADL based on
- the union F ∪ G of the function symbols of L 1 and L 2 , and - the union R ∪ Q of the relation symbols of L 1 and L 2 ,
and M 1 & M 2 is defined as
{ | W, F 20 ∪ G 20 , R 20 ∪ Q 20 ⟩ | ⟨ W, F 20 , R 20 ⟩ ∈ M 1 and  ⟨ W, G 20 , Q 20 ⟩ ∈ M 2 }.

As an example, consider the ADSs S 1 and S 2 corresponding to the DLs ALCF and ALC+,°,µ introduced in Section 2. We concentrate on the function symbols provided by their fusion. In the following, we assume that the set of role names employed by ALCF
and ALC+,°,¤ are disjoint

- The ADS S 1 is based on the following function symbols: (i) unary functions symbol fvR and f 3R for every role name R of ALCF, (ii) nullary functions symbols corresponding to the same-as constructor for every pair of ains of functional roles of ALCF.

- The ADS S 2 is based on the following function symbols: (iii) unary functions symbol fvQ and f 3Q for every role description Q built from role names of ALC + , , , , u using union, composition, and transitive closure.
Since we assumed that the set of role names employed by ALCF and ALC+,°,µ are disjoint, these sets of function symbols are also disjoint.  The union of these sets provides us both with the symbols for the same-as constructor and with the symbols for value and existential restrictions on role descriptions involving union, composition, and transitive closure.

However, the role descriptions contain only role names from ALC+,,,, and thus none of the functional roles of ALCF occurs in such descriptions. Thus, the fusion of ALCF and ALC+,°,µ yields a strict fragment of their union ALCF+,°,µ

## 4.1 Relativized Satisfiability

We prove a transfer result for decidability of the relativized satisfiability problem, show that this also yields a corresponding transfer result for the relativized term satisfiability problem, and investigate how these transfer results can be extended to ADSs that correspond to DLs providing for the universal role.