which can clearly be majorized by 2 p ( n ) for an appropriate polynomial p .  This shows membership in 2 EXP TIME.

The argument regarding the space complexity is similar. Here one must additionally take into account that doubly exponentially many choices can be enumerated using an exponentially large counter.

D

## 4.1.2  T H E  R E L A T V I Z E D  T E R M  S A T I S F I A B I L I T Y  P R O B L E M

The statement of Theorem 17 itself does not imply a transfer result for the relativized term stisfiability problem. The problem is that decidability of the relativized term satisfiability problem in S 1 and S 2 does not necessarily imply decidability of the relativized satisfiability problem in these ADSs, and thus the prerequisite for the theorem to apply is not satisfied.

However, if we consider the statement of Theorem 20, then it is easy to see that this theorem also yields a transfer result for the relativized term satisfiability problem. Corollary 22. Let S 1 and S 2 be local ADSs, and suppose that the relativized term satisfiability problems for S1 and S2 are decidable. Then the relativized term satisfiability problem for S 1 8 S 2 is also decidable.

Proof. Consider the satisfiability criterion in Theorem 20. If we are interested in relativized term satisfiability, then Γ is of the form { a : t} ∪ Γ ′ , where Γ ′ is a set of term assertions. In this case, the sets of assertions Γ 1 and Γ 2 do not contain object assertions involving relations. Now, assume that Γ is of the form { α 1 : t 1 , . . , α n : t n } ∪ Γ i , where Γ i is a set of term assertions. Since two assertions of the form b : s 1 , b : s 2 are equivalent to one assertion b : s 1 A s 2 , we may assume that the a i are distinct from each other. Since S i is local, it is easy to see that the following are equivalent:

$\mathrm{T}$ 2. 
$$\mathbf{P}$$
$$\mathbf{i}\quad\mathbf{\partial}\cdot\mathbf{j}$$
1. {al : tl, ..., an : tn } U F, is satisfiable in Sj.

2. {aj : tj} U Fj is satisfiable in Sj for all j = 1, . . , n.

Since (1 -> 2) is trivial, it is enough to show (2 -> 1). Given models Mj E Mj of {aj :
t j } U Γ j (j = 1 , . . ,n), their disjoint union also belongs to M j , and it is clearly a model of
{a1 : t1, . . ,an : tn} U L',
The second condition can now be checked by applying the term satisfiability test in S i n times.

D

## 4.1.3 Dealing With The Universal Role

As stated above (Proposition 15), ADSs corresponding to DLs with the universal role are not local, and thus Theorem 17 cannot be applied directly. Nevertheless, in some cases this theorem can also be used to obtain a decidability result for fusions of DLs with the universal role, provided that both of them provide for a universal role. (We will comment on the usefulness of this approach in more detail in Section 5.4).

Definition 23. Given an ADS S = ( L , M ), we denote by S U the ADS obtained from S by 1. extending L with two function symbols f 3 U S and f V U S , and