Why is there a need for cyclic proofs?

Question

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?

Answer 1

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).