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.

我们引入了一种适用于大量描述逻辑（DLs）的构造方法，用于建立基于推理系统的基于概念的 Beth 可定义性性质（CBP）。我们以高度表达能力的 DL RIQ 作为案例研究，引入了 RIQ 本体的新颖推理演算，并展示了如何从推理演算证明中计算出某些插值器，这样可以提取出隐含可定义概念的明确定义。据我们所知，这是第一种基于推理系统的计算插值器和定义的方法，也是 RIQ 享受 CBP 的第一个证明。此外，由于我们推理系统的模块化性质，我们的结果对于 RIQ 的任何限制都成立，并且可以通过适当的修改适用于其他 DLs。