Abstract
Motivated primarily by medical terminology applications, the prominent DL SHIQ has already been extended to a DL with com plex role inclusion axioms of the form R ◦ S ˙ ⊑ R or S ◦ R ˙ ⊑ R, called RIQ, and the SHIQ tableau algorithm has been extended to handle such inclusions. This paper further extends RIQ and its tableau algorithm with im portant expressive means that are frequently requested in ontology ap plications, namely with reflexive, symmetric, transitive, and irreflexive roles, disjoint roles, and the construct ∃R.Self, allowing, for instance, the definition of concepts such as a “narcist”. Furthermore, we extend the al gorithm to cover Abox reasoning extended with negated role assertions. The resulting logic is called SRIQ.