循环证明的削减消除:时间逻辑的案例研究
Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic
Bahareh Afshari (University of Gothenburg), Johannes Kloibhofer (University of Amsterdam)
arXiv
2024年5月3日
我们认为模态逻辑与众所周知的时间运算符“最终”扩展,并为捕获此片段的循环隐式演算提供剪切消除程序。 这项工作展示了还原剪切方法对循环微积分的适应。 值得注意的是,提议的算法适用于循环证明,并直接输出循环无切无证明,而不会吸引中间机械对最终证明进行规范化。
We consider modal logic extended with the well-known temporal operator 'eventually' and provide a cut-elimination procedure for a cyclic sequent calculus that captures this fragment. The work showcases an adaptation of the reductive cut-elimination method to cyclic calculi. Notably, the proposed algorithm applies to a cyclic proof and directly outputs a cyclic cut-free proof without appealing to intermediate machinery for regularising the end proof.