<p>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.</p>

<p>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 <a href="http://www.era.lib.ed.ac.uk/bitstream/1842/3394/1/0002.pdf">this paper</a> by Bundy.</p>

<p>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 <em>without</em> 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 <a href="http://www0.cs.ucl.ac.uk/staff/J.Brotherston/TABLEAUX05/cyclic_proofs_folind.pdf">this paper</a> for a comparison between cyclic and non-cyclic proofs (for first-order logic with inductive predicates).</p>

CC BY-SA 3.0
2013-01-14T22:29:44.430Z
2013-01-14T22:29:44.430Z
James Brotherston
<p>I was reading a paper <a href="http://www0.cs.ucl.ac.uk/staff/J.Brotherston/APLAS12/cyclist.pdf" rel="nofollow">A Generic Cyclic Theorem Prover</a>. 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? </p>

CC BY-SA 3.0
2013-01-14T04:17:54.933Z
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
CC BY-SA 3.0
2013-01-14T21:50:56.003Z
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 http://goo.gl/6rv30 The alternative is to _discover_ which induction works. But, let's see if the authors correct me. ;)
Radu GRIGore
<proof-theory>
Why is there a need for cyclic proofs?
Sadiksha Gautam
# Why is there a need for cyclic proofs?

(Asked by: username_0 on 2013-01-13)

I was reading a paper [A Generic Cyclic Theorem Prover](http://www0.cs.ucl.ac.uk/staff/J.Brotherston/APLAS12/cyclist.pdf). 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?

**Tags:** proof-theory

> **Comments:**
> **username_1**: 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. :)  
> **username_2**: 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 http://goo.gl/6rv30 The alternative is to _discover_ which induction works. But, let's see if the authors correct me. ;)  

---

## 1 answers

### Answer by username_3 on 2013-01-14. Score: 9 | Accepted answer

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](http://www.era.lib.ed.ac.uk/bitstream/1842/3394/1/0002.pdf) 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](http://www0.cs.ucl.ac.uk/staff/J.Brotherston/TABLEAUX05/cyclic_proofs_folind.pdf) for a comparison between cyclic and non-cyclic proofs (for first-order logic with inductive predicates).


---

