Next: Domino Systems Up: The Complexity of Reasoning Previous: The Logic ALCQI

Consistency of $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}$ - $\ensuremath {\text {T\hspace {-1pt}}_C\hspace {-1pt}\text {Boxes}}$ is NExpTime-complete

To show that $\textsc{NExp\-Time}$ is also the lower bound for the complexity of $\ensuremath{\text{T\hspace{-1pt}}_C\hspace{-1pt}\text{Box}}$ consistency, we use a bounded version of the domino problem. Domino problems [Wan63,Ber66] have successfully been employed to establish undecidability and complexity results for various description and modal logics [Spa93,BS99].

Domino Systems
Defining a Torus of Exponential Size
Reducing Domino Problems to TBox Consistency

Stephan Tobies
May 02 2000

Consistency of - is NExpTime-complete

Consistency of $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}$ - $\ensuremath {\text {T\hspace {-1pt}}_C\hspace {-1pt}\text {Boxes}}$ is NExpTime-complete