Skip to main content
Unpublished Paper
Tableau Algorithm for Concept Satisfiability in Description Logic ALCH
Kno.e.sis Publications
  • Satya S. Sahoo, Wright State University - Main Campus
  • Krishnaprasad Thirunarayan, Wright State University - Main Campus
Document Type
Report
Publication Date
7-1-2009
Abstract
The provenir ontology is an upper-level ontology to facilitate interoperability of provenance information in scientific applications. The description logic (DL) expressivity of provenir ontology is ALCH, that is, it models role hierarchies (H) (without transitive roles and inverse roles). Even though the complexity results for concept satisfiability for numerous variants of DL such as ALC with transitively closed roles (ALCR+ also called S), inverse roles SI, and role hierarchy SHI have been well-established, similar results for ALCH has been surprisingly missing from the literature. Here, we show that the complexity of the concept satisfiability problem for the ALCH variant of DL is PSpace complete. This result contributes towards a complete set of complexity results for DL variants and establishes a lower bound on complexity for domain-specific provenance ontologies that extend provenir ontology.
Comments

Kno.e.sis Research Center Technical Report TR-2009-07

Citation Information
Satya S. Sahoo and Krishnaprasad Thirunarayan. "Tableau Algorithm for Concept Satisfiability in Description Logic ALCH" (2009)
Available at: http://works.bepress.com/tk_prasad/95/