2. extending every ADM M = {W, F M , R M } E M with the unary functions f H js and fW where
* $f_{\overline{\mathfrak{U}}_{S}}^{\mathfrak{M}}(X)=\emptyset$ if $X=\emptyset$, and $f_{\overline{\mathfrak{U}}_{S}}^{\mathfrak{M}}(X)=W$ otherwise; * $f_{\overline{\mathfrak{U}}_{S}}^{\mathfrak{M}}(X)=W$ if $X=W$, and $f_{\overline{\mathfrak{U}}_{S}}^{\mathfrak{M}}(X)=\emptyset$ otherwise.  
For ADSs S corresponding to a DL L, the ADS S U corresponds to the extension of L
with the universal role, where the universal role can only be used within value and existential restrictions. 8 There is a close connection between the relativized satisfiability problem in S
and the satisfiability problem in SU Proposition 24. If S is a local ADS, then the following conditions are equivalent:
1. the relativized (term) satisfiability problem for S is decidable, 2. the (term) satisfiability problem for SU is decidable, 3. the relativized (term) satisfiability problem for SU is decidable.

Proof. We restrict our attention to the term satisfiability problem since the equivalences for the satisfiability problem can be proved similarly.

The implication (3 → 2) is trivial, and (2 → 1) is easy to show. In fact, t is satisfiable in S relative to the term assertions { s 1 , . . . , s n ⊂ t n } iff t ∧ f v U s . ((¬ t 1 V s 1 ) ∧ . . ∧(¬ t n V s n ))
is satisfiable in SU
To show (1 → 3), we assume that the relativized term satisfiability problem for S is decidable. Let S = (L, M) and S U = (LU, MU). In the following, we use f U as an abbreviation for f v s . Since we can replace equivalently in any term the function symbol fau s by ¬ f U ¬ , we may assume without loss of generality that f 3 U s does not occur in terms of LU.

Suppose a set Σ = { a : s} ∪Γ from L ∪ is given, where Γ is a set of term assertions. We want to decide whether Σ is satisfiable in some model M E M U . To this purpose, we transform Σ into a set of assertions not containing f U . The idea underlying this transformation is that, given a model W ∈ M U , we have f U (t) W ∈ { W, 0}, depending on whether t 2W = W
or not.  Consequently, if we replace fu (t) accordingly by T or ⊥, the evaluation of this term in D does not change. However, in the satisfiability test we do not have the model D (we are trying to decide whether one exists), and thus we must guess the right replacement.

A term t from L U is called a U-term iff it starts with f U . The set of U-terms that occur (possibly as subterms) in Σ is denoted by Σ U .  Set, inductively, for any function