next up previous
Next: ALCQIO Up: Complexity Results Previous: Complexity Results

ALCQ and ALCQO

In [De 95] complexity results for various DLs are obtained by sophisticated polynomial reduction to a propositional dynamic logic. The author establishes many complexity results, one of which is of special interest for our purposes.

Theorem 4.6 ([De 95], Section 7.3)
Satisfiability and logical implication for $\mathcal{C\!N\!O}$ knowledge bases (TBox and ABox) are \textsc{Exp\-Time}-complete.

The DL $\mathcal{C\!N\!O}$ studied by the author is a strict extension of \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{O}}; TBoxes in his thesis correspond to what we call \ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Boxes}} in this paper. Unary coding of numbers is assumed throughout his thesis. Although a unique name assumption is made, it is not inherent to the utilised reduction since is explicitly enforced. It is thus possible to eliminate the propositions that require a unique interpretation of individuals from the reduction. Hence, together with Lemma 4.2, we get the following corollary.

Corollary 4.7
Consistency of \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{O}}- \ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Boxes}} is \textsc{Exp\-Time}-complete if unary coding of number is assumed.

Together with Theorem 4.5, this solves the open problem concerning the lower bound for the complexity of \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}} with cardinality restrictions; moreover, it shows that the \textsc{NExp\-Time}-algorithm presented in [BBH96] is not optimal with respect to worst case complexity.

Corollary 4.8
Consistency of \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}- \ensuremath {\text {T\hspace {-1pt}}_C\hspace {-1pt}\text {Boxes}} is \textsc{Exp\-Time}-complete, if unary coding of numbers in cardinality and number restrictions is used.


next up previous
Next: ALCQIO Up: Complexity Results Previous: Complexity Results

Stephan Tobies
May 02 2000