and CLAIM 1: For every x ∈ ∆ X and every ALCQIO-concept C, we have x ∈ ( C sp y ) X iff x ∈ C X .

We proof this claim by induction on the structure of C .  The only interesting case is C = ( ≥ n R D ). In this case C spy = ( ≥ n R ( ∃ spy¯ i ) ∩ D spy ). We have

x E (≥ n R (∃ spy¯ i ) ∩ D spy ) Z iff  ¦{y ∈ Δ T | (x, y) ∈ R T and y ∈ (∃ spy¯ .i) T ∩ ( D spy) Z } ≥ n (*) iff  ¦{y ∈ Δ T  | (x,y) ∈ R T  and y ∈ D T } ≥ n iff x E (> n R D) T
where the equivalence ( ∗ ) holds because of set equality and the definition of T ′ .

By construction, for every T E C E T and every x E A T , x E ( C 8PY ) T . Due to Claim 1, this implies x ∈ C X and hence I ′ | T ⊆ C .

For the only-if-direction, let I be an interpretation with I |= T . We pick an arbitrary element a ∈ Δ T and define an extension T of I by setting i T = { a } and spy T = { ( a, x ) | x E A T . Since i and spy do not occur in T , we still have that I ′ |= T .

CLAIM 2: For every x E A T and every ALCQIO-concept C that does not contain i or spy, x E C T  iff x E (C 8 PY ) Z ' .

Again, this claim is proved by induction on the structure of concepts and the only interesting case is C = (> n R D).

x E (> n R D) T

$\left.\right.$   iff $\left.\frac{i}{2}\{y\in\Delta^{\mathcal{I}}\mid(x,y)\in R^{\mathcal{I}}\right.$ and $y\in D^{\mathcal{I}}\right\}\geqslant n$  $\left.\right.$ iff $\left.\frac{i}{2}\{y\in\Delta^{\mathcal{I}}\mid(x,y)\in R^{\mathcal{I}},(a,y)\in spy^{\mathcal{I}}\right.$, and $y\in(D^{\,spy})^{\mathcal{I}}\right\}\geqslant n$   iff $x\in(\geqslant n\ R\ (\exists spy^{-},i)\sqcap D^{spy})^{\mathcal{I}}$.  
Again, the equivalence (*) holds due to set equality and the definition of T ′ .

Since, for every T ⊆ C ∈ T, we have I ′ ├ T ⊆ C, Claim 2 yields that ( Π T ⊆ C ET C 8 PY ) T  =
∆ T  and hence α E ( CT ) T
As a consequence, we obtain the sharper result that already pure concept satisfiability for ALCQIO is a NEXPTIME-complete problem.

## Corollary 4.13 Concept Satisfiability For Alcqio Is Nexp Time-Complete.

Proof.  From Lemma 4.12, we get that the function mapping a ALCQIO-T;Box T to C T
is a reduction from consistency of ACCIO-T t Boxes to ACCIO-concept satisfiability. From Corollary 4.9 we know that the former problem is NEXPTIME-complete. Obviously, CT can be computed from T in polynomial time. Hence, the lower complexity bound transfers.

n