Extending Consequence-Based Reasoning to SRIQ
Artificial Intelligence
2016-02-25 v3
Abstract
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.
Cite
@article{arxiv.1602.04498,
title = {Extending Consequence-Based Reasoning to SRIQ},
author = {Andrew Bate and Boris Motik and Bernardo Cuenca Grau and František Simančík and Ian Horrocks},
journal= {arXiv preprint arXiv:1602.04498},
year = {2016}
}