循环证明系统中替换规则的可容许性
计算机科学中的逻辑
2025-10-17 v1
摘要
本文研究了循环证明系统中替换规则的可容许性。替换规则会使理论上的分情况分析变得复杂,并增加证明搜索的计算成本,因为每个序贯都可能是替换规则某实例的结论;因此,从这两个方面来看,可容许性都是可取的。在非循环系统中,可容许性通常通过局部证明变换来证明,但此类变换可能会破坏循环结构,因此并不容易适用。早先的评述曾指出,替换规则在带归纳谓词的一阶逻辑循环证明系统 CLKID^ω 中很可能不可容许。在本文中,我们在假设存在切割(cut)规则的前提下,证明了其在 CLKID^ω 中的可容许性。我们的方法将一个循环证明展开为无穷形式,提升替换规则,并放置回边以构造一个不含替换规则的循环证明。若将替换限制为排除函数符号,该结果可推广到更广泛的系统类,包括无切割的 CLKID^ω 以及分离逻辑的循环证明系统。
引用
@article{arxiv.2510.14749,
title = {Admissibility of Substitution Rule in Cyclic-Proof Systems},
author = {Kenji Saotome and Koji Nakazawa},
journal= {arXiv preprint arXiv:2510.14749},
year = {2025}
}
备注
20 pages, 4 figures(Including the derivation trees inserted within the main text, there are 8 JPEG files)