Decidability of SHIQ with complex role inclusion axioms

https://doi.org/10.1016/j.artint.2004.06.002Get rights and content
Under an Elsevier user license
open archive

Abstract

Motivated by medical terminology applications, we investigate the decidability of an expressive and prominent description logic (DL), SHIQ, extended with role inclusion axioms of the form RS˙T. It is well known that a naive such extension leads to undecidability, and thus we restrict our attention to axioms of the form RS˙R or SR˙R, which is the most important form of axioms in the applications that motivated this extension. Surprisingly, this extension is still undecidable. However, it turns out that by restricting our attention further to acyclic sets of such axioms, we regain decidability. We present a tableau-based decision procedure for this DL and report on its implementation, which promises to behave well in practice and provides important additional functionality in a medical terminology application.

Keywords

Description logics
Tableau algorithm
Automated reasoning

Cited by (0)

This is an extended version of the conference paper [I. Horrocks, U. Sattler, in: Proc. of the 17th Int. Joint Conf. on Artificial Intelligence, IJCAI-03, Morgan Kaufmann, Los Altos, 2003, a long version is available as technical report LTCS 02-06 at http://lat.inf.tu-dresden.de/research/reports.html].