Rippling: A heuristic for guiding inductive proofs
From MaRDI portal
Publication:685548
DOI10.1016/0004-3702(93)90079-QzbMATH Open0789.68121DBLPjournals/ai/BundySHIS93OpenAlexW2087028873WikidataQ56840271 ScholiaQ56840271MaRDI QIDQ685548FDOQ685548
Authors: Alan Bundy, Andrew Stevens, Frank van Harmelen, Andrew Ireland, Alan Smaill 
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
Recommendations
Cites Work
- Proving termination with multiset orderings
- Title not available (Why is that?)
- A Transformation System for Developing Recursive Programs
- Title not available (Why is that?)
- Experiments with proof plans for induction
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automated deduction -- CADE-11. Proceedings of the 11th international conference held in Saratoga Springs, NY, USA, June 15--18, 1992
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Extensions to the rippling-out tactic for guiding inductive proofs
- Guiding induction proofs
- The OYSTER-CLAM system
Cited In (48)
- Rule-based induction
- Title not available (Why is that?)
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- Deaccumulation techniques for improving provability
- An approach to automatic deductive synthesis of functional programs
- A divergence critic
- Function definition in higher-order logic
- Higher-order annotated terms for proof search
- A pragmatic approach to reuse in tactical theorem proving
- On process equivalence = equation solving in CCS
- The use of embeddings to provide a clean separation of term and annotation for higher order rippling
- Extensions to the rippling-out tactic for guiding inductive proofs
- Sound generalizations in mathematical induction
- Using induction and rewriting to verify and complete parameterized specifications
- Case-analysis for rippling and inductive proof
- Verifying procedural programs via constrained rewriting induction
- Theorem Proving in Higher Order Logics
- An integrated approach to high integrity software verification
- Supporting the formal verification of mathematical texts
- Extensions to a generalization critic for inductive proof
- Managing structural information by higher-order colored unification
- Patching faulty conjectures
- Termination of algorithms over non-freely generated data types
- Productive use of failure in inductive proof
- Lemma discovery in automating induction
- A calculus for and termination of rippling
- Artificial Intelligence and Symbolic Computation
- A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs
- Constraint solving for proof planning
- INKA: The next generation
- The automation of proof by mathematical induction
- Title not available (Why is that?)
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
- Dynamic rippling, middle-out reasoning and lemma discovery
- A case study in the mechanical verification of fault tolerance
- A recursion planning analysis of inductive completion
- TIP: tools for inductive provers
- Lazy generation of induction hypotheses
- Termination orderings for rippling
- Getting saturated with induction
- Connection-driven inductive theorem proving
- Mechanizable inductive proofs for a class of \(\forall \exists\) formulas
- Induction and Skolemization in saturation theorem proving
- Title not available (Why is that?)
- Proving theorems by reuse
- Middle-out reasoning for synthesis and induction
- Internal analogy in theorem proving
- A colored version of the \(\lambda\)-calculus
Uses Software
This page was built for publication: Rippling: A heuristic for guiding inductive proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685548)
