| Summary: | <p>Consequence-based (CB) reasoners combine ideas from resolution and
(hyper)tableau calculi to solve the problem of ontology classification in
Description Logics (DLs). Existing CB reasoners, however, are only capable of handling DLs without nominals (such as SRIQ), or DLs without
disjunction (such as Horn-SROIQ). In this thesis, we present a novel
CB calculus for concept subsumption in the DL ALCHOIQ<sup>+</sup>, a logic
that 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: the calculus is worst-case optimal for many well-known fragments of ALCHOIQ<sup>+</sup>, including ELH, Horn-ALCHOIQ<sup>+</sup>, and ALCHIQ<sup>+</sup>. Furthermore, the calculus is worst-case time exponential for the full logic ALCHOIQ<sup>+</sup>, except for cases where nominals, inverse roles, and number restrictions interact simultaneously, which are very rare in practice. Our calculus can also decide DL reasoning problems other than subsumption, such as ontology classification, instance retrieval, and realisation. We have implemented our calculus as an extension of the reasoner Sequoia, which previously supported ontology classification for SRIQ. Our implementation includes novel optimisation techniques that overcome some of the performance limitations affecting the previous version. We have carried out an empirical evaluation of our implementation which shows that the performance of Sequoia is competitive with other state-of-the-art systems. Our results also show that Sequoia nicely complements tableau-based reasoners, as it can more easily classify some ontologies. Thus, the calculus and implementation presented in this thesis provide an important addition to the repertoire of reasoning techniques and practical systems for expressive DLs.</p>
|
|---|