The Circularity Principle was successfully applied for developing a coinductive proving technique, known as circular coinduction. In this paper, we show that the same principle can be used to develop an inductive proving technique. A main advantage of this uniform approach is that the two proving techniques can be easily combined during the verification process. Circular induction is simple, flexible, generic, and therefore it is a good candidate framework for combining different proving schemes into a competitive tool. We exhibit this potential by presenting how the circular induction is implemented in CIRC, a prover built around the Circularity Principle. Disclaimer. This paper was written in 2010, at the time the CIRC prover was developed, and the main body reflects the state of the work and of the prover as of that date. For this arXiv technical report, only the related-work discussion (Section 6) and the concluding section have been revised: Section 6 has been extended to situate circular induction within the cyclic-proof and infinite-descent literature that has appeared or matured since 2010. No other part of the paper-its definitions, results, proofs, examples, or implementation description-has been modified, and the technical content should be read as a 2010 contribution. References to developments after 2010 appear only in the updated related-work section.
翻译:循环性原则已成功应用于开发一种余归纳证明技术,即循环余归纳。本文表明,相同原则也可用于开发归纳证明技术。这种统一方法的主要优势在于,在验证过程中可以轻松组合这两种证明技术。循环归纳简单、灵活且通用,因此是结合不同证明方案形成竞争性工具的优良框架。我们通过展示循环归纳如何在CIRC(一个基于循环性原则构建的证明器)中实现来体现这一潜力。免责声明:本文写于2010年,即CIRC证明器开发之时,主体内容反映了当时的工作和证明器状态。为本次arXiv技术报告,仅修订了相关工作讨论(第6节)和结论部分:第6节已扩展,将循环归纳置于2010年以来出现或成熟的循环证明与无限下降文献中。论文其他部分——其定义、结果、证明、示例或实现描述——均未修改,技术内容应视为2010年的贡献。2010年后的发展参考文献仅出现在更新的相关工作部分。