# Extending Consequence-Based Reasoning to SRIQ

arXiv: https://arxiv.org/abs/1602.04498 · HTML: https://mlsanity.com/paper/1602.04498/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Feb 2016.

## Built on by (most cited first, 3 of 3)

- [On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (Extended Version)](https://mlsanity.com/paper/2206.07711/) (2022)
- [OWL Reasoners still useable in 2023](https://mlsanity.com/paper/2309.06888/) (2023)
- [Neuro-symbolic learning over OWL 2 DL via consequence-based compilation to differentiable circuits](https://mlsanity.com/paper/2608.17741/) (2026)

## Abstract (arXiv)

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.