RIQ and SROIQ are harder than SHOIQ

Abstract. 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. The