Decidability of SHIQ with Complex Role Inclusion Axioms

Motivated by medical terminology applications, we investigate the decidability of the well known expressive DL, SHIQ, extended with role inclusion axioms (RIAs) of the form R ◦ S P. We show that this extension is undecidable even when RIAs are restricted to the forms R◦S R or S ◦R R, but that decidability can be regained by further restricting RIAs to be acyclic. We present a tableau algorithm for this DL and report on its implementation, which behaves well in practise and provides important additional functionality in a medical terminology application. 1 Motivation The description logic (DL) SHIQ [Horrocks et al., 1999; Horrocks and Sattler, 2002b] is an expressive knowledge representation formalism that extends ALC [Schmidt-Schauß and Smolka, 1991] (a notational variant of the multi modal logic K [Schild, 1991]) with qualifying number restrictions, inverse roles, role inclusion axioms (RIAs) R S, and transitive roles. The development of SHIQ was motivated by several applicati...

• Type: Conference
• Year: 2003
• Where: IJCAI
• Authors: Ian Horrocks, Ulrike Sattler
• Keywords: IJCAI 2003, IJCAI 2007, Medical Terminology, Medical Terminology Application, Role Inclusion Axioms