使用标号矢列演算证明 Craig 与 Lyndon 插值
Proving Craig and Lyndon Interpolation Using Labelled Sequent Calculi
AI总结：
本文将证明 Craig 与 Lyndon Interpolation 的方法扩展至标号矢列演算，提供了基于 Kripke-frame 表征的充分准则，并证明无量词 Horn 公式可定义的框架类对应具有 IPs 的逻辑，涵盖模态立方体与传递 Geach 逻辑族。
摘要：
我们近期提出了一种通用方法，通过对广泛类别的内部矢列演算（包括矢列、超矢列和嵌套矢列）中的推导进行归纳，来证明 Craig 与 Lyndon Interpolation (IPs) 这一基本逻辑性质。在此，我们将该方法适配至更一般的标号矢列外部形式体系，并提供了关于逻辑的 Kripke-frame 表征的充分准则以保证 IPs。特别地，我们证明由无量词 Horn 公式可定义的框架类对应于具有 IPs 的逻辑。这些准则涵盖了模态立方体及无限的传递 Geach 逻辑族。
英文摘要：
We have recently presented a general method of proving the fundamental logical properties of Craig and Lyndon Interpolation (IPs) by induction on derivations in a wide class of internal sequent calculi, including sequents, hypersequents, and nested sequents. Here we adapt the method to a more general external formalism of labelled sequents and provide sufficient criteria on the Kripke-frame characterization of a logic that guarantee the IPs. In particular, we show that classes of frames definable by quantifier-free Horn formulas correspond to logics with the IPs. These criteria capture the modal cube and the infinite family of transitive Geach logics.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
