Rippling: Meta-Level Guidance for Mathematical Reasoning

DOI10.1017/CBO9780511543326zbMath1095.68108OpenAlexW1992696924MaRDI QIDQ5462949

Alan Bundy, Dieter Hutter, Andrew Ireland, David A. Basin

Publication date: 28 July 2005

Full work available at URL: https://doi.org/10.1017/cbo9780511543326

zbMATH Keywords

ripplingproof planningtheorem-provingautomating reasoning

Mathematics Subject Classification ID

Related Items (30)

\textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema} ⋮ Verifying Procedural Programs via Constrained Rewriting Induction ⋮ Proof mining with dependent types ⋮ Automating Induction with an SMT Solver ⋮ Security of multi-agent systems: a case study on comparison shopping ⋮ Hints in Unification ⋮ An integrated approach to high integrity software verification ⋮ A proof-centric approach to mathematical assistants ⋮ The problem of \(\Pi_{2}\)-cut-introduction ⋮ On the generation of quantified lemmas ⋮ Algorithmic introduction of quantified cuts ⋮ Conjecture synthesis for inductive theories ⋮ Automated theorem provers: a practical tool for the working mathematician? ⋮ Recycling proof patterns in Coq: case studies ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ An approach to automatic deductive synthesis of functional programs ⋮ Synthesis of list algorithms by mechanical proving ⋮ Reasoning about Assignments in Recursive Data Structures ⋮ Automating Event-B invariant proofs by rippling and proof patching ⋮ Synthesis of sorting algorithms using multisets in \textit{Theorema} ⋮ Narrowing Based Inductive Proof Search ⋮ Deduction as an Engineering Science ⋮ The use of embeddings to provide a clean separation of term and annotation for higher order rippling ⋮ Verification by Parallelization of Parametric Code ⋮ Automated search for Gödel's proofs ⋮ Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery ⋮ Confluence by critical pair analysis revisited ⋮ Ours Is to Reason Why ⋮ Inductive theorem proving based on tree grammars ⋮ PLANS AND PLANNING IN MATHEMATICAL PROOFS

This page was built for publication: Rippling: Meta-Level Guidance for Mathematical Reasoning