Rippling: A heuristic for guiding inductive proofs

DOI10.1016/0004-3702(93)90079-QzbMath0789.68121OpenAlexW2087028873WikidataQ56840271 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

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, 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item