can be performed in linear time, the NEXPTIME upper bound (Grädel et al., 1997; Pacholski et al., 1997) for satisfiability of C 2 directly carries over to ACCQI-T c Box consistency:
Lemma 2.2 Consistency of an ALCQI-T c Box T can be decided in NEXPTIME.

Please note that the NEXPTIME-completeness result from (Pacholski et al., 1997) is only valid if we assume unary coding of numbers in the input; this implies that a number n may not be stored in logarithmic space in some k -ary representation but consumes n units of storage. This is the standard assumption made by most results concerning the complexity of DLs. We will come back to this issue in Section 3.3.

## 3. Consistency Of Acci-T C Boxes Is Nexptime-Complete

To show that NEXPTIME is also the lower bound for the complexity of T C Box consistency, we use a bounded version of the domino problem. Domino problems (Wang, 1963; Berger, 1966) have successfully been employed to establish undecidability and complexity results for various description and modal logics (Spaan, 1993; Baader & Sattler, 1999).

## 3.1 Domino Systems

Definition 3.1 For n E N, let Z, denote the set {0,...,n –1} and B, denote the addition modulo n. A domino system is a triple D = ( D, H, V ), where D is a finite set (of tiles)
and H, V ⊆ D × D are relations expressing horizontal and vertical compatibility constraints between the tiles.  For s,t E N, let U(s,t) be the torus Z s × Z i , and let w = w 0 . . . w n − 1 be a word over D of length n (with n < s). We say that D tiles U(s,t) with initial condition w iff there exists a mapping τ : U ( s, t ) → D such that, for all ( x, y ) ∈ U ( s, t ),
- if T(x, y) = d and T(x Bs 1, y) = d', then (d, d') E H  (horizontal constraint);

- if T(x, y) = d and T(x, y Bt 1) = d', then (d, d') E V  (vertical constraint);
- T(i, 0) = wi for 0 < i < n (initial condition).
Bounded domino systems are capable of expressing the computational behaviour of restricted, so-called simple, Turing Machines (TM). This restriction is non-essential in the following sense: Every language accepted in time T ( n ) and space S ( n ) by some one-tape TM
is accepted within the same time and space bounds by a simple TM, as long as S(n), T(n) ≥
2n (Borger et al., 1997).

Theorem 3.2 ((Börger et al., 1997), Theorem 6.1.2)
Let M be a simple TM with input alphabet E. Then there exists a domino system D =
(D, H,V) and a linear time reduction which takes any input x ∈ Σ * to a word w ∈ D * with |x| = | w | such that
- If M accepts x in time to with space so, then D tiles U ( s, t ) with initial condition w for all s ≥ so + 2, t ≥ to + 2;

- if M does not accept x, then D does not tile U ( s, t ) with initial condition w for any s, t ≥ 2.