Rippling: Meta-Level Guidance for Mathematical Reasoning

From MaRDI portal
Revision as of 11:02, 9 February 2024 by Import240129110113 (talk | contribs) (Created automatically from import240129110113)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Publication:5462949

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




Related Items (30)

\textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema}Verifying Procedural Programs via Constrained Rewriting InductionProof mining with dependent typesAutomating Induction with an SMT SolverSecurity of multi-agent systems: a case study on comparison shoppingHints in UnificationAn integrated approach to high integrity software verificationA proof-centric approach to mathematical assistantsThe problem of \(\Pi_{2}\)-cut-introductionOn the generation of quantified lemmasAlgorithmic introduction of quantified cutsConjecture synthesis for inductive theoriesAutomated theorem provers: a practical tool for the working mathematician?Recycling proof patterns in Coq: case studiesMathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017An approach to automatic deductive synthesis of functional programsSynthesis of list algorithms by mechanical provingReasoning about Assignments in Recursive Data StructuresAutomating Event-B invariant proofs by rippling and proof patchingSynthesis of sorting algorithms using multisets in \textit{Theorema}Narrowing Based Inductive Proof SearchDeduction as an Engineering ScienceThe use of embeddings to provide a clean separation of term and annotation for higher order ripplingVerification by Parallelization of Parametric CodeAutomated search for Gödel's proofsDynamic Rippling, Middle-Out Reasoning and Lemma DiscoveryConfluence by critical pair analysis revisitedOurs Is to Reason WhyInductive theorem proving based on tree grammarsPLANS AND PLANNING IN MATHEMATICAL PROOFS







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