by a description of the form 3 ( xoy Πy ox ). T, where x, y are features.  In fact, this description expresses that the "points" belonging to it have both an x o y and a y o x successor, and that these two successors coincide. Accessing all point on the grid can then be achieved by using the role description ( x ∪ y )+.

Note that this undecidability result is also closely related to the known undecidability of IDPDL, i.e., deterministic propositional dynamic logic with intersection (Harel, 1984).

However, the undecidability proof for IDPDL by Harel (1984) uses the test construct, which is not available in ALC t,°,¤,¤
Next, we show that relativized satisfiability in two rather expressive sublanguages of ACt ° ∩ ¬ is decidable.

Theorem 38. Relativized satisfiability of concept descriptions is decidable in ALC † , °, ¹ and AC+,°,¤,¤
Proof sketch. In both cases, TBoxes can be internalized as described by Schild (1991)
and Baader et al. (1993).  Thus, it is sufficient to show decidability of (unrelativized)
satisfiability.

For ALC + 10 11 , this follows from decidability of DPDL (Ben-Ari, Halpern, & Pnueli, 1982), the known correspondence between PDL and ALC+,°,°,° (Schild, 1991), and the fact that non-functional roles can be simulated by functional ones in the presence of composition and transitive closure (Parikh, 1980).

For ALC+,°,µ, decidability of satisfiability follows from decidability of IPDL, i.e., PDL
with intersection (Danecki, 1984).

o Given this theorem, Corollary 22 now yields the following decidability result.

Corollary 39. Relativized satisfiability of concept descriptions is decidable in the fusion AC ‡ ° ' ¹ ® ALC + ° '

## 5.3 A "Concrete" Example

Description logics with concrete domains were introduced by Baader and Hanschke (1991)
in order to allow for the reference to concrete objects like numbers, time intervals, spatial regions, etc. when defining concepts.  To be more precise, Baader and Hanschke (1991)
define the extension ALC ( D ) of ALC , where D is a concrete domain (see below). Under suitable assumptions on D , they show that satisfiability in ALC(D) is decidable.  One of the main problems with this extension of DLs is that relativized satisfiability (and satisfiability in DLs where TBoxes can be internalized) is usually undecidable (Baader & Hanschke, 1992) (though there are exceptions, see Lutz, 2001). For this reason, Haarslev et al. (2001)
introduce a restricted way of extending DLs by concrete domains, and show that the corresponding extension of ALCNHR+ has a decidable relativized satisfiability problem. 10  In the following, we show that this result can also be obtained as an easy consequence of