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

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 38 references that are in the map.
- First posted on arXiv 24 Apr 2024.

## Builds on (most cited first, 5 of 5)

- [Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents](https://mlsanity.com/paper/1910.05215/) (2019)
- [Living Without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions](https://mlsanity.com/paper/2007.02736/) (2020)
- [On Free Description Logics with Definite Descriptions](https://mlsanity.com/paper/2106.15513/) (2021)
- [Nested Sequents for Intuitionistic Modal Logics via Structural Refinement](https://mlsanity.com/paper/2107.01998/) (2021)
- [Display to Labeled Proofs and Back Again for Tense Logics](https://mlsanity.com/paper/1911.02289/) (2019)

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

- [Interpolation in Knowledge Representation](https://mlsanity.com/paper/2512.08833/) (2025)

## Abstract (arXiv)

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.