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 any restriction of RIQ, and are applicable to other DLs by suitable modifications.

翻译：我们提出一种适用于大量描述逻辑的构造性方法，用于基于相继式系统建立基于概念的贝斯可定义性性质。以高表达力的描述逻辑 RIQ 作为案例研究，我们为 RIQ-本体引入了新型相继式演算，展示了如何从相继式演算证明中计算出某些插值，从而能够提取隐式可定义概念的显式定义。据我们所知，这是首个在描述逻辑背景下计算插值和定义的基于相继式的方法，也是首个证明 RIQ 具有基于概念的贝斯可定义性的工作。此外，由于我们相继式系统的模块化特性，我们的结果适用于 RIQ 的任何限制，并通过适当修改可应用于其他描述逻辑。