our Theorem 17. Moreover, ALCNHR+ can be replaced by an arbitrary local DL with a decidable relativized satisfiability problem.

Definition 40 (Concrete Domain). A concrete domain D is a pair ( DD, PD ), where ∆ D
is a nonempty set called the domain, and Φ D is a set of predicate names. Each predicate nme P E Φ D is associated with an arity n and an n-ary predicate P D ⊆ ∆ n . A concrete domain D is called admissible iff (1) the set of its predicate names is closed under negation and contains a name T D for A D , and (2) the satisfiability problem for finite conjunctions of predicates is decidable.

Given a concrete domain D and one of the predicates P E Φ D (of arity n ), one can define a new concept constructor ∃ f 1 , . . , f n . P (predicate restriction), where f 1 , . . , f n are concrete features. 11 In contrast to the abstract features considered until now, concrete features are interpreted by partial functions from the abstract domain A T into the concrete domain AD. We consider the basic DL that allows for Boolean operators and these new concept constructors only.

Definition 41 ( B ( D )). Let N C be a set of concept names and N F , be a set of names for concrete features disjoint from Nc, and let D be an admissible concrete domain. Concepts descriptions of B ( D ) are Boolean combinations of concept names and predicate restrictions, i.e., expressions of the form ∃ f 1 , . . , f n . P where P is an n -ary predicate in Φ D and fir . . . fn E N F .

The semantics of B ( D ) is defined as follows. We consider an interpretation I , which has a nonempty domain ∆ T , and interprets concept names as subsets of ∆ T and concrete features as partial functions from A T into A D . The Boolean operators are interpreted as usual, and

$(\exists f_{1},\ldots,f_{n}.P)^{\mathcal{I}}=\{a\in\Delta^{\mathcal{I}}\mid\exists x_{1},\ldots,x_{n}\in\Delta_{\mathcal{D}}.\}$
$f_{i}^{\mathcal{I}}(a)=x_{i}$ for all $1\leq i\leq n$ and $(x_{1},\ldots,x_{n})\in P^{\mathcal{D}}$.  
Note that concept descriptions are interpreted as subsets of A T and not of A T U A T .

Thus, if we go to the ADS corresponding to B ( D ), the concrete domain is not an explicit part of the corresponding ADMs. It is only used to define the interpretation of the function symbols corresponding to predicate restrictions.  The predicate restriction constructor is translated into a function symbol f 3 f 1 to a frame I, f I f , ....f . , P is defined as ( ∃ f 1 , . . , f n . P ) Z θ , where Z q is the interpretation based on f that maps all concept names to the empty set. Theorem 42. Let D be an admissible concrete domain. Then, B(D) is local and the relativized satisfiability problem for B(D)-concept descriptions is decidable. Proof.    Given the family ( M i ) i E I of ADMs W i corresponding to the frames & over pairwise disjoint domains A δ i ( i ∈ I ), we first build the union & of the frames: the domain of & is Ujcj Δ δ i and it interprets the concrete features in the obvious way, i.e., f δ ( x ) := f δ i ( x ) if