SRIQ and SROIQ are Harder than SHOIQ

We identify the complexity of (finite model) reasoning in the DL SROIQ to be N2ExpTime-complete. We also prove that (finite model) reasoning in the DL SR--a fragment of SROIQ without nominals, number restrictions, and inverse roles--is 2ExpTime-hard. 1 From SHIQ to SROIQ In this paper we study the complexity of reasoning in the DL SROIQ--the logic chosen as a candidate for OWL 2.1 SROIQ has been introduced in [1] as an extension of SRIQ, which itself was introduced previously in [2] as an extension of RIQ [3]. These papers present tableau-based procedures for the respective DLs and prove their soundness, completeness and termination. In contrast to sub-languages of SHOIQ whose computational complexities are currently well understood [4], almost nothing was known, up until now, about the complexity of SROIQ, SRIQ and RIQ except for the hardness results inherited from their sub-lanbuages: SROIQ is NExpTime-hard as an extension of SHOIQ, SRIQ and RIQ are ExpTime-hard as extensions of SHIQ...

• Type: Conference
• Year: 2008
• Where: DLOG
• Authors: Yevgeny Kazakov
• Keywords: Automated Reasoning, DLOG 2008, Finite Model, Reasoning, Role Inclusion Axioms