SHOIQ with transitive closure of roles is decidable

Abstract : The Semantic Web makes an extensive use of the OWL DL ontology language, underlied by the SHOIQ description logic, to formalize its resources. In this paper, we propose a decision procedure for this logic extended with the transitive closure of roles in concept axioms, a feature needed in several application domains. To address the problem of consistency in this logic, we introduce a new structure for characterizing models which may have an infinite non-tree-like part.