Consequence-based reasoning for description logics with disjunctions and number restrictions

Description logics (DLs) are a family of knowledge representation formalisms that provide the logical foundation of the OWL 2 DL ontology language. Effcient ontology classification lies at the core of many practical applications of DLs, so considerable effort has been devoted to the development and optimisation of practical reasoning calculi. Consequence-based calculi combine ideas from hypertableau and resolution in a way that has proved very effective in practice; for example, the CB reasoner used such a calculus to classify the GALEN ontology and thus solved a long-standing open DL reasoning problem. Since then, the development of consequence-based reasoning calculi and their implementation in practical reasoners have attracted considerable attention. Existing consequence-based calculi, however, can handle either Horn DLs (which do not support disjunction) or DLs without number restrictions. In this paper, we overcome this important limitation and present the first consequence-based calculus for deciding concept subsumption in the DL ALCHIQ+, which supports all Boolean connectives, self-restrictions, number restrictions, role hierarchies, and inverse and reflexive roles; since we focus on concept subsumption, we do not consider ABox axioms. Our calculus runs in exponential time assuming unary coding of numbers, and on ELH ontologies it runs in polynomial time. The extension to disjunctions and number restrictions is technically involved because the relevant consequences cannot be captured using DLs themselves; instead, we capture these consequences using first-order clauses and adapt the paramodulation techniques from first-order theorem proving. By using a well-known preprocessing step, the calculus can also decide concept subsumptions in SRIQ|a rich DL covering all features of OWL 2 DL apart from nominals and datatypes. We have implemented our calculus in a new reasoner called Sequoia. We present the architecture of our reasoner and discuss important implementation techniques such as clause indexing and redundancy elimination. Finally, we present the results of an extensive performance evaluation that showed Sequoia to be competitive with existing reasoners. Thus, the calculus and the techniques we present in this paper provide an important addition to the repertoire of practical implementation techniques for description logic reasoning