Tableau Algorithm for Concept Satisfiability in Description Logic ALCH

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 (ALC _R+ 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.