FOLID循环预证明中回链的验证
计算机科学中的逻辑
2018-10-18 v1
摘要
循环预证明可以表示为带有回链的有限树推导的集合。在一阶归纳定义逻辑(FOLID)的框架下,树推导的节点由相继式标记,回链将特定的终结节点(称为芽)连接到其他由相同相继式标记的节点。然而,只有部分回链能构成可靠的预证明。先前已表明,沿表示循环预证明特定正规形的有向图的最小圈所定义的特殊序和推导条件,足以验证回链。在该方法中,处理不同最小圈时同一约束可能被多次检查,因此可能需要额外的记录机制以避免冗余计算,从而将时间复杂度降至多项式。我们提出一种不需要处理最小圈的新方法。它基于一种正规形,该正规形允许仅通过考虑其有向图的非单点强连通分量的根-芽路径来定义验证条件。
引用
@article{arxiv.1810.07374,
title = {Validating Back-links of FOLID Cyclic Pre-proofs},
author = {Sorin Stratulat},
journal= {arXiv preprint arXiv:1810.07374},
year = {2018}
}
备注
In Proceedings CL&C 2018, arXiv:1810.05392