Automating induction over mutually recursive functions

Deepak Kapur, M. Subramaniam

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Scopus citations


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 languageEnglish (US)
Title of host publicationAlgebraic Methodology and Software Technology - 5th International Conference, AMAST 1996, Proceedings
EditorsMartin Wirsing, Maurice Nivat
PublisherSpringer Verlag
Number of pages15
ISBN (Print)9783540614630
StatePublished - 1996
Externally publishedYes
Event5th International Conference on Algebraic Methodology and Software Technology, AMAST 1996 - Munich, Germany
Duration: Jul 1 1996Jul 5 1996

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other5th International Conference on Algebraic Methodology and Software Technology, AMAST 1996

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Automating induction over mutually recursive functions'. Together they form a unique fingerprint.

Cite this