An ExpSpace Tableau-based Algorithm for SHOIQ

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

In this paper, we propose an EXPSPACE tableau-based algorithm for SHOIQ. The construction of this algorithm is founded on the standard tableau-based method for SHOIQ and the technique used for designing a NEXPTIME algorithm for the two-variable fragment of first-order logic with counting quantifiers C2 .

Mots clés: Reasoning; Ontology; Description Logic

Domaines: Intelligence artificielle [cs.AI]

Chan Le Duc, Myriam Lamolle, Olivier Curé. An ExpSpace Tableau-based Algorithm for SHOIQ. Description Logic 2012, Jun 2012, Rome, Italy. pp.11. ⟨hal-00799028⟩