Extending Consequence-Based Reasoning to SRIQ
This work addresses a limitation in automated reasoning for knowledge representation, though it appears incremental as it extends existing calculi to a richer logic.
The paper tackled the problem of extending consequence-based reasoning to SRIQ, a description logic that supports disjunction and counting quantifiers, by presenting a novel calculus and showing preliminary feasibility results.
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.