A Tableaux-Based Algorithm for SHIQ with Transitive Closure of Roles in Concept and Role Inclusion Axioms

Abstract : In this paper, we investigate an extension of the description logic SHIQ -a knowledge representation formalism used for the Semantic Web-with transitive closure of roles occurring not only in concept inclusion axioms but also in role inclusion axioms. It was proved that adding transitive closure of roles to SHIQ without restriction on role hierarchies may lead to undecidability. We have identified a kind of role inclusion axioms that is responsible for this undecidability and we propose a restriction on these axioms to obtain decidability. Next, we present a tableaux-based algorithm that decides satisfiability of concepts in the new logic.