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

Presented at: 8th Extended Semantic Web Conference (ESWC2011)

by Chan Le Duc, Myriam Lamolle, Olivier Curé

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.

Keywords: Description Logics, OWL, Reasoning, Tableaux, Transitive closure

Resource URI on the dog food server: http://data.semanticweb.org/conference/eswc/2011/paper/reasoning/2

Explore this resource elsewhere: