Consequence-based Reasoning for Description Logics with Disjunction, Inverse Roles, Number Restrictions, and Nominals

TL;DR

This paper introduces a consequence-based reasoning calculus for complex description logics like ALCHOIQ and SROIQ, enabling efficient concept subsumption and classification with a pay-as-you-go approach.

Contribution

It presents a novel consequence-based calculus that is worst-case optimal for key fragments of ALCHOIQ, extending to SROIQ, with a flexible, incremental reasoning strategy.

Findings

Achieves worst-case optimality for important logic fragments

Extends to SROIQ, covering OWL 2 DL features

Offers a pay-as-you-go reasoning approach

Abstract

We present a consequence-based calculus for concept subsumption and classification in the description logic ALCHOIQ, which extends ALC with role hierarchies, inverse roles, number restrictions, and nominals. By using standard transformations, our calculus extends to SROIQ, which covers all of OWL 2 DL except for datatypes. A key feature of our calculus is its pay-as-you-go behaviour: unlike existing algorithms, our calculus is worst-case optimal for all the well-known proper fragments of ALCHOIQ, albeit not for the full logic.