Decidability of an Expressive Description Logic with Rational Grading

TL;DR

This paper introduces part restrictions with rational grading into a Description Logic, extending its expressiveness while maintaining decidability, and provides a tableau-based reasoning method for the extended logic.

Contribution

It extends ALCQIHR+ with part restrictions and proves that reasoning remains decidable using a novel tableaux technique with indices.

Findings

Reasoning in the extended logic is decidable.

Tableaux technique with indices is effective for handling part restrictions.

The extension enhances DL expressiveness without sacrificing computational properties.

Abstract

In this paper syntactic objects---concept constructors called part restrictions which realize rational grading are considered in Description Logics (DLs). Being able to convey statements about a rational part of a set of successors, part restrictions essentially enrich the expressive capabilities of DLs. We examine an extension of well-studied DL ALCQIHR+ with part restrictions, and prove that the reasoning in the extended logic is still decidable. The proof uses tableaux technique augmented with indices technique, designed for dealing with part restrictions.