| Summary: | Consequence-based (CB) reasoners combine ideas from resolution and (hyper)tableau calculi for solving key reasoning problems
in Description Logics (DLs), such as ontology classification. Existing CB reasoners, however, are only capable of handling DLs
without nominals (such as ALCHIQ), or DLs without disjunction (such as Horn-ALCHOIQ). In this paper, we present a
consequence-based calculus for concept subsumption and classification in the DL ALCHOIQ+
, which extends ALC with role
hierarchies, inverse roles, number restrictions, and nominals; to the best of our knowledge, ours is the first CB calculus for an
NExpTime-complete DL. By using standard transformations, our calculus extends to SROIQ, which covers all of OWL 2 DL
except for datatypes. A key feature of our calculus is its pay-as-you-go behaviour: our calculus is worst-case optimal for all
the well-known proper fragments of ALCHOIQ+
. Furthermore, our calculus can be applied to DL reasoning problems other
than subsumption and ontology classification, such as instance retrieval and realisation. We have implemented our calculus as
an extension of Sequoia, a CB reasoner which previously supported ontology classification in SRIQ. We have performed an
empirical evaluation of our implementation, which shows that Sequoia offers competitive performance. Although there still
remains plenty of room for further optimisation, the calculus presented in this paper and its implementation provide an important
addition to the repertoire of reasoning techniques and practical systems for expressive DLs.
|
|---|