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.

翻译：我们提出了一种适用于大量描述逻辑的构造性方法，该方法基于序列系统来建立概念式Beth可定义性。以高度表达性的描述逻辑RIQ作为案例研究，我们为RIQ本体引入了新颖的序列演算系统，并展示了如何从序列演算证明中计算特定插值式，从而允许从隐式可定义概念中提取显式定义。据我们所知，这是在描述逻辑背景下首个基于序列计算插值与定义的方法，同时也是首次证明RIQ满足概念式Beth可定义性。此外，由于我们的序列系统具有模块化特性，所得结果适用于RIQ的任何限制片段，并可通过适当修改应用于其他描述逻辑。