# 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. :) Commented Jan 14, 2013 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. ;) Commented Jan 14, 2013 at 21:50