# Why is there a need for cyclic proofs?

I was reading a paper A Generic Cyclic Theorem Prover. This paper explains about automated theorem prover based on various instantiations like the notion of first order logic equations with inductive definitions using cyclic proofs. I was unable to understand about why cyclic proofs are required. As far as I understand, sometime with the induction rules, we can go to an infinite loop, to avoid this condition of going into infinite loop, they introduced cyclic proofs. Can anyone please correct me if I am wrong?

-
It would be nice if you can explain what is a cyclic proof for those of us who are not familiar with the topic so we can also understand the question. :) –  Kaveh Jan 14 '13 at 4:17
Very briefly, I think the point is that you discover the induction principle that is good to use while searching for the proof, rather than first selecting an induction principle and then trying to see if you can build a proof. Suppose you want to prove that the sum of two even numbers is even. You could use induction on natural numbers, or you could use induction on even numbers, as done here: Coq'Art, section 8.3.3 goo.gl/6rv30 The alternative is to discover which induction works. But, let's see if the authors correct me. ;) –  Radu GRIGore Jan 14 '13 at 21:50

In order to reason about inductively defined objects (numbers, lists, trees...), one needs to use induction, or some principle that is at least as powerful as induction.

But explicit induction rules cause huge difficulties for automatic proof search, because they typically force you to invent the necessary induction schema and induction hypotheses at the beginning of the proof. For some discussion of these difficulties, see this paper by Bundy.

Cyclic proof is an alternative to explicit induction; that is, instead of using a standard proof system with explicit induction rules, one can use a cyclic proof system without explicit induction rules. This allows a somewhat more exploratory approach to proof search, where the induction argument is essentially created implicitly through the discovery of a cyclic proof. See this paper for a comparison between cyclic and non-cyclic proofs (for first-order logic with inductive predicates).

-