Decidability of SHIQ with Complex Role Inclusion Axioms

11 years 1 months ago
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...
Ian Horrocks, Ulrike Sattler
Added 31 Oct 2010
Updated 31 Oct 2010
Type Conference
Year 2003
Authors Ian Horrocks, Ulrike Sattler
Comments (0)