Tableau Algorithm for Concept Satisfiability in Description Logic ALCH

TitleTableau Algorithm for Concept Satisfiability in Description Logic ALCH
Publication TypeMiscellaneous
Year of Publication2009
AuthorsSatya S. Sahoo, Krishnaprasad Thirunarayan
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.

Full Text

Satya S. Sahoo, Krishnaprasad Thirunarayan, 'Tableau Algorithm for Concept Satisfiability in Description Logic ALCH', Kno.e.sis Center Technical Report knoesis-TR-2009-07, July, 2009
year: 2009
hasURL: http://knoesis.wright.edu/library/download/DL-ALCHConceptSatisfiability_...