





















Abstract: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.
| Comments: | 17 pages, 2 figures, 1 table |
| Subjects: | Logic in Computer Science (cs.LO); Software Engineering (cs.SE) |
| Cite as: | arXiv:2605.24968 [cs.LO] |
| (or arXiv:2605.24968v1 [cs.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2605.24968 arXiv-issued DOI via DataCite (pending registration) |
From: Dorel Lucanu [view email]
[v1]
Sun, 24 May 2026 09:44:50 UTC (37 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理,仅供阅读参考。 原文来自 — 版权归原作者所有。