pith. sign in

arxiv: 2605.24968 · v1 · pith:2MFD3UKVnew · submitted 2026-05-24 · 💻 cs.LO · cs.SE

Circular Induction

Dorel Lucanu , Grigore Rosu , Eugen Goriac , Georgiana Caltais This is my paper

Pith reviewed 2026-06-29 23:59 UTC · model grok-4.3

classification 💻 cs.LO cs.SE
keywords circular inductioncircularity principlecircular coinductioninductive provingcoinductive provingproof combinationCIRC prover
0
0 comments X

The pith

The Circularity Principle can be adapted to develop a sound inductive proving technique that combines easily with circular coinduction.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that the Circularity Principle, already used to create circular coinduction, directly supports an analogous inductive proof method called circular induction. This uniform treatment lets inductive and coinductive steps be mixed freely inside a single verification run. The resulting technique is presented as simple, flexible, and generic enough to serve as a base for merging multiple proof schemes, with the CIRC prover serving as the concrete implementation.

Core claim

The Circularity Principle can be used to develop circular induction, a proving technique for inductive properties that parallels circular coinduction. The adaptation requires no substantial additional conditions or changes to the underlying logic, so that the two techniques can be combined without friction during verification.

What carries the argument

The Circularity Principle, which justifies assuming a goal as a hypothesis and deriving the goal from that assumption in a circular derivation.

If this is right

  • Induction and coinduction steps can be interleaved freely inside one verification process.
  • Circular induction supplies a uniform framework for integrating distinct proving schemes.
  • The approach is realized directly in the CIRC prover built around the Circularity Principle.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The uniformity could reduce engineering effort when building tools that must reason about both finite and infinite structures.
  • The same circularity mechanism might be lifted to other formalisms that already contain circular coinduction.
  • Implementation details in CIRC could be reused as a template for adding circular induction to existing inductive provers.

Load-bearing premise

The Circularity Principle can be directly adapted from its coinductive use to induction without requiring substantial additional conditions or changes to the logic.

What would settle it

An inductive property that is valid yet cannot be proved by the circular induction rules, or an unsound derivation that the rules accept as a proof.

Figures

Figures reproduced from arXiv: 2605.24968 by Dorel Lucanu, Eugen Goriac, Georgiana Caltais, Grigore Rosu.

Figure 1
Figure 1. Figure 1: Intuitive proof by circular induction even(n) = evenm(n) even(0 ) = evenm(0 ) true = true ✓ even(s(n1)) = evenm(s(n1)) even(s(n1)) = oddm(n1) even(s(0 )) = oddm(0 ) false = false✓ even(s(s(n2))) = oddm(s(n2)) even(n2) = evenm(n2) 0 s( ) 0 s( ) n2 ∼ n [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Intuitive proof by circular induction The proof of the conjecture (∀N)even(N ) = evenm(N ) is intuitively represented by the graph in [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Duality between circular coinduction and circular induction in the basic entailment relation, which allows using circular induction as framework suitable to combine more proving techniques. The structure of the paper is as follows. In Section 2 we present some preliminary notions used through￾out the paper, including a brief recall of the circular coinduction in order to facilitate the comparison of the tw… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper claims that the Circularity Principle, previously used to develop circular coinduction, can be directly adapted to yield a sound circular induction technique. A key advantage is that inductive and coinductive proofs can be freely interleaved within the same CIRC prover; the manuscript describes the technique's implementation in CIRC and presents it as simple, flexible, and generic for combining proving schemes.

Significance. If the adaptation holds, the uniform Circularity Principle framework enables straightforward mixing of induction and coinduction during verification, which could support more competitive automated tools. The concrete implementation in CIRC supplies a working demonstration of the approach.

minor comments (3)
  1. [Abstract] Abstract: the central claim is stated at a high level without any definitions, proof sketches, or small examples, which makes the technical contribution hard to evaluate from the abstract alone (though the full manuscript supplies these).
  2. [Disclaimer] Disclaimer (and §1): the note that only the related-work section and conclusion were revised is useful, but the introduction should explicitly flag that all definitions, theorems, and implementation details remain exactly as in the 2010 version.
  3. [Introduction] The related-work section (now updated) situates the work in the cyclic-proof literature, but a brief forward reference from the introduction to §6 would help readers locate the modern context.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of the manuscript, the recognition of its potential advantages for interleaving inductive and coinductive proofs, and the recommendation of minor revision. No specific major comments appear in the report.

Circularity Check

0 steps flagged

No significant circularity; direct adaptation of prior principle

full rationale

The paper presents circular induction as an adaptation of the pre-existing Circularity Principle (originally for coinduction) without introducing self-referential definitions, fitted predictions, or load-bearing self-citations that reduce the central claim to its own inputs. The abstract states the principle 'was successfully applied' for coinduction and 'can be used' for induction, with the disclaimer confirming the technical content is unchanged from 2010. No equations or steps in the provided material exhibit the enumerated circular patterns; the derivation remains self-contained against the cited external principle.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the assumption that the Circularity Principle extends from coinduction to induction; this is treated as a domain assumption rather than derived within the paper.

axioms (1)
  • domain assumption The Circularity Principle applies to inductive proofs in the same manner as to coinductive proofs
    Invoked in the abstract as the basis for developing the new technique from the coinductive version.

pith-pipeline@v0.9.1-grok · 5763 in / 1056 out tokens · 34315 ms · 2026-06-29T23:59:30.773565+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

23 extracted references · 13 canonical work pages

  1. [1]

    Bouhoula, A.: Automated theorem proving by test set induction. J. Symb. Comput.23(1), 47–77 (1997), https://doi.org/10.1006/jsco.1996.0076

    work page doi:10.1006/jsco.1996.0076 1997

  2. [2]

    In: Alagar, V.S., Nivat, M

    Bouhoula, A., Rusinowitch, M.: SPIKE: A system for automatic inductive proofs. In: Alagar, V.S., Nivat, M. (eds.) Algebraic Methodology and Software Technology, 4th International Conference, AMAST ’95, Montreal, Canada, July 3-7, 1995, Proceedings. pp. 576–577. Lecture Notes in Computer Science, Springer (1995), https://doi.org/10.1007/3-540-60043-4_79

    work page doi:10.1007/3-540-60043-4_79 1995

  3. [3]

    In: M¨ uller-Olm, M., Seidl, H

    Brotherston, J., Gorogiannis, N.: Cyclic abduction of inductively defined safety and termination precon- ditions. In: M¨ uller-Olm, M., Seidl, H. (eds.) Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings. pp. 68–84. Lecture Notes in Computer Science, Springer (2014),https://doi.org/10.1007/978-3-3...

    work page doi:10.1007/978-3-319-10936-7_5 2014

  4. [4]

    In: Jhala, R., Igarashi, A

    Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Jhala, R., Igarashi, A. (eds.) Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings. pp. 350–367. Lecture Notes in Computer Science, Springer (2012),https: //doi.org/10.1007/978-3-642-35182-2_25

    work page doi:10.1007/978-3-642-35182-2_25 2012

  5. [5]

    Brotherston & A

    Brotherston, J., Simpson, A.: Complete sequent calculi for induction and infinite descent. In: 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings. pp. 51–62. IEEE Computer Society (2007),https://doi.org/10.1109/LICS.2007.16

    work page doi:10.1109/lics.2007.16 2007

  6. [6]

    In: Robinson, J.A., Voronkov, A

    Bundy, A.: The automation of proof by mathematical induction. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 845–911. Elsevier and MIT Press (2001),https: //doi.org/10.1016/b978-044450813-3/50015-1

    work page doi:10.1016/b978-044450813-3/50015-1 2001

  7. [7]

    (eds.): All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, vol

    Clavel, M., Dur´ an, F., Eker, S., Lincoln, P., Mart´ ı-Oliet, N., Meseguer, J., Talcott, C.L. (eds.): All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, vol. 4350. Springer (2007)

    2007

  8. [8]

    In: Peltier, N., Sofronie-Stokkermans, V

    Cohen, L., Rowe, R.N.S.: Integrating induction and coinduction via closure operators and proof cycles. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I. pp. 375–394. Lecture Notes in Computer Science, Springer (2020),https://doi.org/10...

    work page doi:10.1007/978-3-030-51074-9_21 2020

  9. [9]

    In: Gurfinkel, A., Heule, M

    Cohen, L., Rowe, R.N.S., Shaked, M.: Cyclone: A heterogeneous tool for verifying infinite descent. In: Gurfinkel, A., Heule, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, O...

    work page doi:10.1007/978-3-031-90643-5_18 2025

  10. [10]

    In: Robinson, J.A., Voronkov, A

    Comon, H.: Inductionless induction. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 913–962. Elsevier and MIT Press (2001),https://doi.org/10.1016/ b978-044450813-3/50016-3

    2001

  11. [11]

    In: Bruni, A., Momigliano, A., Pradella, M., Rossi, M., Cheney, J

    Dur´ an, F.J., Escobar, S., Meseguer, J., Sapi˜ na, J.: Nuitp: An inductive theorem prover for equational program verification. In: Bruni, A., Momigliano, A., Pradella, M., Rossi, M., Cheney, J. (eds.) Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, PPDP 2024, Milano, Italy, September 9-11, 2024. pp. ...

    work page doi:10.1145/3678232.3678236 2024

  12. [12]

    In: LPAR

    Falke, S., Kapur, D.: Inductive decidability using implicit induction. In: LPAR. Lecture Notes in Computer Science, vol. 4246, pp. 45–59. Springer (2006)

    2006

  13. [13]

    Caltais, E

    G. Caltais, E. Goriac, D.L., Grigora¸ s, G.: A Rewrite Stack Machine forROC!In: 10th International Sympo- sium on Symbolic and Numeric Algorithms for Scientific Computing. IEEE Computer Society (2008)

    2008

  14. [14]

    In: WADT

    Goguen, J., Lin, K., Ro¸ su, G.: Conditional circular coinductive rewriting with case analysis. In: WADT. Lecture Notes in Computer Science, vol. 2755, pp. 216–232. Springer (2002)

    2002

  15. [15]

    Theoretical Computer Science105(2), 217–273 (1992)

    Goguen, J., Meseguer, J.: Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science105(2), 217–273 (1992)

    1992

  16. [16]

    In: 12th International Sym- posium on Symbolic and Numeric Algorithms for Scientific Computing

    Goriac, E., Caltais, G., Lucanu, D.: Simplification and Generalization in CIRC. In: 12th International Sym- posium on Symbolic and Numeric Algorithms for Scientific Computing. IEEE Computer Society (2009)

    2009

  17. [17]

    In: Jhala, R., Dillig, I

    Jones, E., Ong, C.L., Ramsay, S.J.: Cycleq: an efficient basis for cyclic equational reasoning. In: Jhala, R., Dillig, I. (eds.) PLDI ’22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022. pp. 395–409. ACM (2022),https: //doi.org/10.1145/3519939.3523731

    work page doi:10.1145/3519939.3523731 2022

  18. [18]

    https://doi.org/10.5281/zenodo.20345982,https://github.com/ dlucanu/circ

    Lucanu, D.: Circ v1.5 (May 2026). https://doi.org/10.5281/zenodo.20345982,https://github.com/ dlucanu/circ

    work page doi:10.5281/zenodo.20345982 2026

  19. [19]

    In: CALCO 2009

    Lucanu, D., Goriac, E.I., Caltais, G., Ro¸ su, G.: CIRC : A behavioral verification tool based on circular coinduction. In: CALCO 2009. LNCS, vol. 5728, pp. 433–442. Springer (2009)

    2009

  20. [20]

    In: ICFEM

    Lucanu, D., Ro¸ su, G.: Circular coinduction with special contexts. In: ICFEM. LNCS, vol. 5885, pp. 639–659. Springer (2009)

    2009

  21. [21]

    In: Stickel, M.E

    Reddy, U.S.: Term rewriting induction. In: Stickel, M.E. (ed.) 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings. pp. 162–177. Lecture Notes in Computer Science, Springer (1990),https://doi.org/10.1007/3-540-52885-7_86

    work page doi:10.1007/3-540-52885-7_86 1990

  22. [22]

    In: CALCO 2009

    Ro¸ su, G., Lucanu, D.: Circular Coinduction – A Proof Theoretical Foundation. In: CALCO 2009. LNCS, vol. 5728, pp. 127–144. Springer (2009)

    2009

  23. [23]

    In: Lusk, E.L., Overbeek, R.A

    Zhang, H., Kapur, D., Krishnamoorthy, M.S.: A mechanizable induction principle for equational specifica- tions. In: Lusk, E.L., Overbeek, R.A. (eds.) 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings. pp. 162–181. Lecture Notes in Computer Science, Springer (1988),https://doi.org/10.1007/BFb0012831 17

    work page doi:10.1007/bfb0012831 1988