SRIQ and SROIQ are Harder than SHOIQ.

We identify the computational complexity of (finite model) reasoning in the sublanguages of the description logic SROIQ—the logic currently proposed as the basis for the next version of the web ontology language OWL. We prove that the classical reasoning problems are N2ExpTimecomplete for SROIQ and 2ExpTime-hard for its sublanguage RIQ. RIQ and SROIQ are thus exponentially harder than SHIQ and SHOIQ. The growth in complexity is due to complex role inclusion axioms of the form R1 ◦ · · · ◦ Rn ⊑ R, which are known to cause an exponential blowup in the tableau-based procedures for RIQ and SROIQ. Our complexity results, thus, also prove that this blowup is unavoidable. We also demonstrate that the hardness results hold already for linear role inclusion axioms of the form R1 ◦ R2 ⊑ R1 and R1 ◦ R2 ⊑ R2.