通过矢列演算实现描述逻辑的构造性插值与基于概念的Beth可定义性
Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents
AI总结：
本文提出基于矢列系统的构造性方法，首次证明高表达力描述逻辑RIQ具有基于概念的Beth可定义性，并可从证明中计算插值式以提取隐式概念的显式定义。
摘要：
我们引入一种构造性方法，适用于大量描述逻辑（DLs），用于基于矢列系统建立基于概念的Beth可定义性性质（CBP）。以高表达力的描述逻辑RIQ作为案例研究，我们为RIQ本体引入了新颖的矢列演算，并展示了如何从矢列演算证明中计算某些插值式，从而允许提取隐式可定义概念的显式定义。据我们所知，这是在描述逻辑语境下第一个基于矢列的方法来计算插值式和定义，也是第一个证明RIQ具有CBP的工作。此外，由于我们矢列系统的模块化特性，我们的结果对RIQ的限制版本同样成立，并且通过适当的修改可适用于其他描述逻辑。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
