AI 中文总结
提出新证明理论方法证明林登插值，基于深度推理中分裂引理推广，将插值定理表述为推导的片段分解，应用于多种逻辑并引入新无切割证明系统展示其灵活性。
AI 中文摘要
我们提出了一种新的证明理论方法来证明林登插值。我们的证明不使用相继式演算，而是基于深度推理中分裂引理的推广。然后我们将插值定理表述为一个推导分解为上片段和下片段。这可视作：（i）插值定理标准表述的强化；（ii）切割消去定理的推广。我们通过将其应用于线性逻辑、经典逻辑和模态逻辑来展示该方法的灵活性。为此，我们还在深度推理中为几种模态逻辑引入了新颖的无切割证明系统。
英文摘要
We propose a new proof theoretical method for proving Lyndon interpolation. Our proof does not use the sequent calculus but is based on a generalization of the splitting lemma in deep inference. We then formulate the interpolation theorem as a decomposition of a derivation into an up-fragment and a down-fragment. This can be seen as (i) a strengthening of the standard formulation of the interpolation theorem, and (ii) a generalization of the cut elimination theorem. We demonstrate the flexibility of our approach by applying it to linear logic, classical logic, and modal logics. For this, we also introduce novel cut-free proof systems for several modal logics in deep inference.
