### Abstract

In order to automate proofs by induction a crucial problem that needs to be addressed is to decide on an induction scheme that leads to appropriate induction hypotheses for carrying out the proof. Boyer and Moore proposed in [5] the use of terminating function definitions for generating induction schemes. Inspired by Boyer and Moore's work, Zhang, Kapur and Krishnamoorthy introduced the cover set induction method for mechanizing induction for equational specifications in [14]. Both these approaches do not consider interaction among function definitions. Induction schemes are generated by considering function definitions in isolation, one at a time. In applications involving mutually recursive definitions, exploiting interactions among the definitions seems crucial. The cover set method implemented in the theorem prover RRL [13] as well as the methods implemented for induction in Boyer and Moore's theorem prover Nqthm based on the above approaches, do not perform well when the definitions involved are mutually recursive. Proving even very simple properties over such definitions by these methods requires some form of user intervention. We discuss how the cover set induction method implemented in RRL can be extended to automatically prove inductive properties of mutual recursive functions. An algorithm for generating cover sets from mutually recursive definitions is given. The proposed method has been implemented in the theorem prover RRL and has been extensively experimented with good results. The effectiveness of the method is illustrated using a nontrivial example of showing the equivalence of the call by value and call by name bottom-up evaluation of arithmetic expressions. A comparison of the method with those employed in Nqthm and also with an approach based on implicit induction [7, 3, 2] implemented in the theorem prover Spike is given.

Original language | English (US) |
---|---|

Title of host publication | Algebraic Methodology and Software Technology - 5th International Conference, AMAST 1996, Proceedings |

Editors | Maurice Nivat, Martin Wirsing |

Publisher | Springer Verlag |

Pages | 117-131 |

Number of pages | 15 |

ISBN (Print) | 9783540614630 |

State | Published - Jan 1 1996 |

Event | 5th International Conference on Algebraic Methodology and Software Technology, AMAST 1996 - Munich, Germany Duration: Jul 1 1996 → Jul 5 1996 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 1101 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 5th International Conference on Algebraic Methodology and Software Technology, AMAST 1996 |
---|---|

Country | Germany |

City | Munich |

Period | 7/1/96 → 7/5/96 |

### Fingerprint

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

### Cite this

*Algebraic Methodology and Software Technology - 5th International Conference, AMAST 1996, Proceedings*(pp. 117-131). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1101). Springer Verlag.

**Automating induction over mutually recursive functions.** / Kapur, Deepak; Subramaniam, M.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*Algebraic Methodology and Software Technology - 5th International Conference, AMAST 1996, Proceedings.*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1101, Springer Verlag, pp. 117-131, 5th International Conference on Algebraic Methodology and Software Technology, AMAST 1996, Munich, Germany, 7/1/96.

}

TY - GEN

T1 - Automating induction over mutually recursive functions

AU - Kapur, Deepak

AU - Subramaniam, M.

PY - 1996/1/1

Y1 - 1996/1/1

N2 - In order to automate proofs by induction a crucial problem that needs to be addressed is to decide on an induction scheme that leads to appropriate induction hypotheses for carrying out the proof. Boyer and Moore proposed in [5] the use of terminating function definitions for generating induction schemes. Inspired by Boyer and Moore's work, Zhang, Kapur and Krishnamoorthy introduced the cover set induction method for mechanizing induction for equational specifications in [14]. Both these approaches do not consider interaction among function definitions. Induction schemes are generated by considering function definitions in isolation, one at a time. In applications involving mutually recursive definitions, exploiting interactions among the definitions seems crucial. The cover set method implemented in the theorem prover RRL [13] as well as the methods implemented for induction in Boyer and Moore's theorem prover Nqthm based on the above approaches, do not perform well when the definitions involved are mutually recursive. Proving even very simple properties over such definitions by these methods requires some form of user intervention. We discuss how the cover set induction method implemented in RRL can be extended to automatically prove inductive properties of mutual recursive functions. An algorithm for generating cover sets from mutually recursive definitions is given. The proposed method has been implemented in the theorem prover RRL and has been extensively experimented with good results. The effectiveness of the method is illustrated using a nontrivial example of showing the equivalence of the call by value and call by name bottom-up evaluation of arithmetic expressions. A comparison of the method with those employed in Nqthm and also with an approach based on implicit induction [7, 3, 2] implemented in the theorem prover Spike is given.

AB - In order to automate proofs by induction a crucial problem that needs to be addressed is to decide on an induction scheme that leads to appropriate induction hypotheses for carrying out the proof. Boyer and Moore proposed in [5] the use of terminating function definitions for generating induction schemes. Inspired by Boyer and Moore's work, Zhang, Kapur and Krishnamoorthy introduced the cover set induction method for mechanizing induction for equational specifications in [14]. Both these approaches do not consider interaction among function definitions. Induction schemes are generated by considering function definitions in isolation, one at a time. In applications involving mutually recursive definitions, exploiting interactions among the definitions seems crucial. The cover set method implemented in the theorem prover RRL [13] as well as the methods implemented for induction in Boyer and Moore's theorem prover Nqthm based on the above approaches, do not perform well when the definitions involved are mutually recursive. Proving even very simple properties over such definitions by these methods requires some form of user intervention. We discuss how the cover set induction method implemented in RRL can be extended to automatically prove inductive properties of mutual recursive functions. An algorithm for generating cover sets from mutually recursive definitions is given. The proposed method has been implemented in the theorem prover RRL and has been extensively experimented with good results. The effectiveness of the method is illustrated using a nontrivial example of showing the equivalence of the call by value and call by name bottom-up evaluation of arithmetic expressions. A comparison of the method with those employed in Nqthm and also with an approach based on implicit induction [7, 3, 2] implemented in the theorem prover Spike is given.

UR - http://www.scopus.com/inward/record.url?scp=84886703490&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84886703490&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:84886703490

SN - 9783540614630

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 117

EP - 131

BT - Algebraic Methodology and Software Technology - 5th International Conference, AMAST 1996, Proceedings

A2 - Nivat, Maurice

A2 - Wirsing, Martin

PB - Springer Verlag

ER -