# A Decision Procedure for $\mathcal{SHOIQ}$ with Transitive Closure of Roles

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. The most challenging issue we have to deal with when designing such a decision procedure is to represent infinitely non-tree-shaped models, which are different from those of SHOIQ ontologies. To address this issue, we introduce a new blocking condition for characterizing models which may have an infinite non-tree-shaped part.
Keywords :
Document type :
Conference papers

https://hal-upec-upem.archives-ouvertes.fr/hal-01740560
Contributor : Olivier Curé <>
Submitted on : Thursday, March 22, 2018 - 10:09:56 AM
Last modification on : Tuesday, May 5, 2020 - 11:50:16 AM

### Citation

Chan Le Duc, Myriam Lamolle, Olivier Curé. A Decision Procedure for $\mathcal{SHOIQ}$ with Transitive Closure of Roles. ISWC 2013 - 12th International Semantic Web Conference 2013, 2013, Sydney, Australia. ⟨10.1007/978-3-642-41335-3_17⟩. ⟨hal-01740560⟩