Rippling: A heuristic for guiding inductive proofs

DOI10.1016/0004-3702(93)90079-QzbMath0789.68121DBLPjournals/ai/BundySHIS93OpenAlexW2087028873WikidataQ56840271 ScholiaQ56840271MaRDI QIDQ685548

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

Publication date: 9 May 1994

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

Full work available at URL: https://doi.org/10.1016/0004-3702(93)90079-q

zbMATH Keywords

ripplinginductive proofs

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (33)

Verifying Procedural Programs via Constrained Rewriting Induction ⋮ A case study in the mechanical verification of fault tolerance ⋮ Rule-based induction ⋮ Sound generalizations in mathematical induction ⋮ On process equivalence = equation solving in CCS ⋮ A recursion planning analysis of inductive completion ⋮ An integrated approach to high integrity software verification ⋮ Supporting the formal verification of mathematical texts ⋮ Productive use of failure in inductive proof ⋮ Middle-out reasoning for synthesis and induction ⋮ A calculus for and termination of rippling ⋮ Deaccumulation techniques for improving provability ⋮ Getting saturated with induction ⋮ An approach to automatic deductive synthesis of functional programs ⋮ Proving theorems by reuse ⋮ Using induction and rewriting to verify and complete parameterized specifications ⋮ Extensions to a generalization critic for inductive proof ⋮ Patching faulty conjectures ⋮ Internal analogy in theorem proving ⋮ Termination of algorithms over non-freely generated data types ⋮ INKA: The next generation ⋮ Lemma discovery in automating induction ⋮ The use of embeddings to provide a clean separation of term and annotation for higher order rippling ⋮ Constraint solving for proof planning ⋮ Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction ⋮ A divergence critic ⋮ Lazy generation of induction hypotheses ⋮ Mechanizable inductive proofs for a class of ∀ ∃ formulas ⋮ Termination orderings for rippling ⋮ A colored version of the λ-calculus ⋮ A Pragmatic Approach to Reuse in Tactical Theorem Proving ⋮ Induction and Skolemization in saturation theorem proving ⋮ A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs

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
• Extensions to the rippling-out tactic for guiding inductive proofs
• Guiding induction proofs
• The OYSTER-CLAM system
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Rippling: A heuristic for guiding inductive proofs