Extending Consequence-Based Reasoning to SRIQ
  Consequence-based calculi are a family of reasoning algorithms for
description logics (DLs), and they combine hypertableau and resolution in a way
that often achieves excellent performance in practice. Up to now, however, they
were proposed for either Horn DLs (which do not support disjunction), or for
DLs without counting quantifiers. In this paper we present a novel
consequence-based calculus for SRIQ---a rich DL that supports both features.
This extension is non-trivial since the intermediate consequences that need to
be derived during reasoning cannot be captured using DLs themselves. The
results of our preliminary performance evaluation suggest the feasibility of
our approach in practice.
