论文标题
裁员理论：第一步
A theory of cut-restriction: first steps
论文作者
论文摘要
切除是证明理论的基石。正是这种算法消除了导致无剪切的微积分和应用的序列证明的切割。切除术都适用于许多逻辑，而不论其语义是什么。这就是它的影响，每当在依次的微积分中证明切割时，不变的响应就是转向更丰富的证明系统以恢复它。在本文中，我们研究了一种根本不同的方法：在无法消除时，适应古老的切割灭绝以限制切割形式的形状。我们解决了无剪切的“第一级”：分析削减。我们的方法应用于双关键逻辑和S5的序列计算，其中已知已知的分析削减是必需的。这标志着切割理论的第一步。
Cut-elimination is the bedrock of proof theory. It is the algorithm that eliminates cuts from a sequent calculus proof that leads to cut-free calculi and applications. Cut-elimination applies to many logics irrespective of their semantics. Such is its influence that whenever cut-elimination is not provable in a sequent calculus the invariable response has been a move to a richer proof system to regain it. In this paper we investigate a radically different approach to the latter: adapting age-old cut-elimination to restrict the shape of the cut-formulas when elimination is not possible. We tackle the "first level" above cut-free: analytic cuts. Our methodology is applied to the sequent calculi for bi-intuitionistic logic and S5 where analytic cuts are already known to be required. This marks the first steps in a theory of cut-restriction.
