RIQ and SROIQ are Harder than SHOIQ

Principles of Knowledge Representation and Reasoning: Proceedings of the Eleventh International Conference (KR2008)

Volume

Principles of Knowledge Representation and Reasoning: Proceedings of the Eleventh International Conference (KR2008)

Contents

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 N2ExpTime-complete for SROIQ and 2ExpTime-hard for its sub-language 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 o ... o R_n => 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 o R_2 => R1 and R1 o R_2 => R2.