文章基本信息

标题：A Cyclic Proof System for HFL_â".
本地全文：下载
作者：Mayuko Kori ; Takeshi Tsukada ; Naoki Kobayashi 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2021
卷号：183
页码：29:1-29:22
DOI：10.4230/LIPIcs.CSL.2021.29
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：A cyclic proof system allows us to perform inductive reasoning without explicit inductions. We propose a cyclic proof system for HFL_â"., 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 HFL_â". validity checking.
关键词：Cyclic proof; higher-order logic; fixed-point logic; sequent calculus