The even more irresistible SROIQ

We describe an extension of the description logic underlying OWL-DL, SHOIN, with a number of expressive means that we believe will make it more useful in practise. Roughly speaking, we extend SHOIN with all expressive means that were suggested to us by ontology developers as useful additions to OWL-DL, and which, additionally, do not affect its decidability. We consider complex role inclusion axioms of the form R ◦ S ˙ ⊑ R or S ◦ R ˙ ⊑ R to express propagation of one property along another one, which have proven useful in medical terminologies. Furthermore, we extend SHOIN with reflexive, symmetric, transitive, and irreflexive roles, disjoint roles, a universal role, and constructs ∃R.Self, allowing, for instance, the definition of concepts such as a “narcist”. Finally, we consider negated role assertions in Aboxes and qualified number restrictions. The resulting logic is called SROIQ. We present a rather elegant tableau-based reasoning algorithm: it combines the use of automata to keep track of universal value restrictions with the techniques developed for SHOIQ. We believe that SROIQ could serve as a logical basis for possible future extensions of OWL-DL.