Automatic generation of generalization lemmas for proving properties of tail-recursive definitions

DOI10.1007/10930755_9MaRDI QIDQ3559764zbMATH OpenOpenAlexFDO

Authors Deepak Kapur, Nikita A. Sakhanenko

Publication date 7 May 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/10930755_9

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Lemma discovery in automating induction
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• scientific article; zbMATH DE number 108494
• Automatic verification of functions with accumulating parameters
• Appropriate lemmae discovery

Cited in

(5)

• Equivalence checking of two functional programs using inductive theorem provers
• On the generation of quantified lemmas
• Lemma discovery in automating induction
• Verifying procedural programs via constrained rewriting induction
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation

This page was built for publication: Automatic generation of generalization lemmas for proving properties of tail-recursive definitions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3559764)