论文标题
HFLN的环保系统
A Cyclic Proof System for HFLN
论文作者
论文摘要
环保系统使我们能够执行感应推理而无需明确的归纳。我们为HFLN提出了一个循环证明系统，该系统是具有自然数和交替固定点的高阶谓词逻辑。据我们所知，我们是第一个用于高阶逻辑的环保系统。由于存在高阶谓词和交替的固定点，我们的循环证明系统需要比Grotherston和Simpson的原始系统更精致的环状证明条件。我们证明了检查该系统的全球状况和健全性的可决定性，并且还证明了我们环保系统中无限期变体的标准完整性形式有限。基于Kobayashi等人最近从程序验证到HFLN有效性检查的减少工作，我们的循环证明系统的潜在应用是对高阶程序的半自动验证。
A cyclic proof system allows us to perform inductive reasoning without explicit inductions. We propose a cyclic proof system for HFLN, which is a higher-order predicate logic with natural numbers and alternating fixed-points. Ours is the first cyclic proof system for a higher-order logic, to our knowledge. Due to the presence of higher-order predicates and alternating fixed-points, our cyclic proof system requires a more delicate global condition on cyclic proofs than the original system of Brotherston and Simpson. We prove the decidability of checking the global condition and soundness of this system, and also prove a restricted form of standard completeness for an infinitary variant of our cyclic proof system. A potential application of our cyclic proof system is semi-automated verification of higher-order programs, based on Kobayashi et al.'s recent work on reductions from program verification to HFLN validity checking.
