SHOIQ with transitive closure of roles is decidable

Chan Le Duc (1) , Myriam Lamolle (1) , Olivier Curé (2)

1 LIASD - Laboratoire d'Informatique Avancée de Saint-Denis
2 LIGM - Laboratoire d'Informatique Gaspard-Monge

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.

Domaines: Intelligence artificielle [cs.AI]

Chan Le Duc, Myriam Lamolle, Olivier Curé. SHOIQ with transitive closure of roles is decidable. Description Logics, 2013, Ulm, Germany. ⟨hal-01740557⟩