next up previous
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].


Stephan Tobies
May 02 2000