Rippling: A heuristic for guiding inductive proofs

DOI10.1016/0004-3702(93)90079-QzbMath0789.68121WikidataQ56840271 ScholiaQ56840271MaRDI QIDQ685548

Alan Bundy, Alan Smaill, Andrew Stevens, Frank van Harmelen, Andrew Ireland

Publication date: 9 May 1994

Published in: Artificial Intelligence (Search for Journal in Brave)

zbMATH Keywords

rippling; inductive proofs

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

Related Items

A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs, A case study in the mechanical verification of fault tolerance, Using induction and rewriting to verify and complete parameterized specifications, An integrated approach to high integrity software verification, Supporting the formal verification of mathematical texts, Deaccumulation techniques for improving provability, Rule-based induction, A recursion planning analysis of inductive completion, Constraint solving for proof planning, Sound generalizations in mathematical induction, Productive use of failure in inductive proof, Middle-out reasoning for synthesis and induction, A calculus for and termination of rippling, Proving theorems by reuse, An approach to automatic deductive synthesis of functional programs

Uses Software

• Nuprl
• CLAM
• Oyster

Cites Work

• Experiments with proof plans for induction
• Automated deduction -- CADE-11. Proceedings of the 11th international conference held in Saratoga Springs, NY, USA, June 15--18, 1992
• Proving termination with multiset orderings
• A Transformation System for Developing Recursive Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item