Automating induction over mutually recursive functions

Deepak Kapur, M. Subramaniam

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

5 Scopus citations

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 languageEnglish (US)
Title of host publicationAlgebraic Methodology and Software Technology - 5th International Conference, AMAST 1996, Proceedings
EditorsMartin Wirsing, Maurice Nivat
PublisherSpringer Verlag
Pages117-131
Number of pages15
ISBN (Print)9783540614630
DOIs
StatePublished - 1996
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)
Volume1101
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other5th International Conference on Algebraic Methodology and Software Technology, AMAST 1996
CountryGermany
CityMunich
Period7/1/967/5/96

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

Cite this