Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper introduces circular induction, an inductive proving technique derived from the Circularity Principle, mirroring the development of circular coinduction. The key advantage lies in its uniformity, facilitating easy combination with coinductive techniques during verification. The authors demonstrate its potential within the CIRC prover, highlighting its simplicity, flexibility, and generality as a framework for integrating diverse proving schemes.
Circular induction offers a uniform approach to inductive and coinductive proving, enabling their seamless integration for enhanced verification processes.
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.