next up previous
Next: Unique Name Assumption Up: Complexity Results Previous: ALCQ and ALCQO

ALCQIO

Conversely, using Theorem 4.5 enables us to transfer the \textsc{NExp\-Time}-completeness result from Theorem 3.8 to \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}.

Corollary 4.9
Consistency of \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}- \ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Boxes}} or \ensuremath {\text {T\hspace {-1pt}}_C\hspace {-1pt}\text {Boxes}} is \textsc{NExp\-Time}-complete.

Proof. For \ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Boxes}}, this is an immediate corollary of Theorem 4.5 and Theorem 3.8. Reasoning with \ensuremath {\text {T\hspace {-1pt}}_C\hspace {-1pt}\text {Boxes}} is as hard as for \ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Boxes}} in the presences of nominals.

This results explains a gap in [De 95]. There the author establishes the complexity of satisfiability of knowledge bases consisting of \ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Boxes}} and ABoxes both for $\mathcal{C\!N\!O}$, which allows for qualifying number restrictions, and for $\mathcal{C\!I\!O}$, which allows for inverse roles, by reduction to an \textsc{Exp\-Time}-complete PDL. No results are given for the combination $\mathcal{C\!I\!N\!O}$, which is a strict extension of \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}. Corollary 4.8 shows that, assuming $\textsc{Exp\-Time}\xspace\neq \textsc{NExp\-Time}\xspace$, there cannot be a polynomial reduction from the satisfiability problem of $\mathcal{C\!I\!N\!O}$ knowledge bases to an \textsc{Exp\-Time}-complete PDL. Again, a possible explanation for this leap in complexity is the loss of the tree model property. While for $\mathcal{C\!I\!O}$ and $\mathcal{C\!N\!O}$, consistency is decided by searching for a tree-like pseudo-models even in the presence of nominals, this seems no longer to be possible in the case of knowledge bases for $\mathcal{C\!I\!N\!O}$.



 
next up previous
Next: Unique Name Assumption Up: Complexity Results Previous: ALCQ and ALCQO

Stephan Tobies
May 02 2000