Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents

TL;DR

This paper presents a constructive sequent calculus approach for establishing the concept-based Beth definability property in description logics, demonstrated on RIQ, enabling explicit concept definitions from proofs.

Contribution

It introduces the first sequent-based method for computing interpolants and definitions in DLs, proving RIQ has the CBP and extending to other DLs via modular sequent systems.

Findings

First sequent calculus for DLs to compute interpolants

Proves RIQ DL has the concept-based Beth definability property

Method applicable to other DLs with modifications

Abstract

We introduce a constructive method applicable to a large number of description logics (DLs) for establishing the concept-based Beth definability property (CBP) based on sequent systems. Using the highly expressive DL RIQ as a case study, we introduce novel sequent calculi for RIQ-ontologies and show how certain interpolants can be computed from sequent calculus proofs, which permit the extraction of explicit definitions of implicitly definable concepts. To the best of our knowledge, this is the first sequent-based approach to computing interpolants and definitions within the context of DLs, as well as the first proof that RIQ enjoys the CBP. Moreover, due to the modularity of our sequent systems, our results hold for restrictions of RIQ, and are applicable to other DLs by suitable modifications.