Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要