Rippling: A heuristic for guiding inductive proofs
From MaRDI portal
Publication:685548
Recommendations
Cites work
- scientific article; zbMATH DE number 4164171 (Why is no real title available?)
- scientific article; zbMATH DE number 4164172 (Why is no real title available?)
- scientific article; zbMATH DE number 4047053 (Why is no real title available?)
- scientific article; zbMATH DE number 4072439 (Why is no real title available?)
- scientific article; zbMATH DE number 1348457 (Why is no real title available?)
- scientific article; zbMATH DE number 1348478 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- A Transformation System for Developing Recursive Programs
- Automated deduction -- CADE-11. Proceedings of the 11th international conference held in Saratoga Springs, NY, USA, June 15--18, 1992
- Experiments with proof plans for induction
- Extensions to the rippling-out tactic for guiding inductive proofs
- Guiding induction proofs
- Proving termination with multiset orderings
- The OYSTER-CLAM system
Cited in
(48)- Internal analogy in theorem proving
- A colored version of the \(\lambda\)-calculus
- Rule-based induction
- scientific article; zbMATH DE number 1863385 (Why is no real title available?)
- Deaccumulation techniques for improving provability
- An approach to automatic deductive synthesis of functional programs
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- A divergence critic
- Function definition in higher-order logic
- Higher-order annotated terms for proof search
- The use of embeddings to provide a clean separation of term and annotation for higher order rippling
- On process equivalence = equation solving in CCS
- A pragmatic approach to reuse in tactical theorem proving
- 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
- An integrated approach to high integrity software verification
- Supporting the formal verification of mathematical texts
- Verifying procedural programs via constrained rewriting induction
- Theorem Proving in Higher Order Logics
- Managing structural information by higher-order colored unification
- Extensions to a generalization critic for inductive proof
- Productive use of failure in inductive proof
- Patching faulty conjectures
- Termination of algorithms over non-freely generated data types
- A calculus for and termination of rippling
- Lemma discovery in automating induction
- 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
- scientific article; zbMATH DE number 1612558 (Why is no real title available?)
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
- Dynamic rippling, middle-out reasoning and lemma discovery
- A recursion planning analysis of inductive completion
- A case study in the mechanical verification of fault tolerance
- TIP: tools for inductive provers
- Lazy generation of induction hypotheses
- Termination orderings for rippling
- Getting saturated with induction
- Connection-driven inductive theorem proving
- Induction and Skolemization in saturation theorem proving
- Mechanizable inductive proofs for a class of \(\forall \exists\) formulas
- Proving theorems by reuse
- scientific article; zbMATH DE number 1389654 (Why is no real title available?)
- Middle-out reasoning for synthesis and induction
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)
