Rippling: Meta-Level Guidance for Mathematical Reasoning
From MaRDI portal
Recommendations
Cited in
(44)- Managing structural information by higher-order colored unification
- The problem of \(\Pi_{2}\)-cut-introduction
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
- Automated search for Gödel's proofs
- A calculus for and termination of rippling
- Synthesis of sorting algorithms using multisets in \textit{Theorema}
- \textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema}
- Confluence by critical pair analysis revisited
- Inductive theorem proving based on tree grammars
- Proof mining with dependent types
- Security of multi-agent systems: a case study on comparison shopping
- On the generation of quantified lemmas
- An approach to automatic deductive synthesis of functional programs
- The automation of proof by mathematical induction
- Ours Is to Reason Why
- Automating Induction with an SMT Solver
- Reasoning about assignments in recursive data structures
- Dynamic rippling, middle-out reasoning and lemma discovery
- Hints in Unification
- Algorithmic introduction of quantified cuts
- scientific article; zbMATH DE number 1348478 (Why is no real title available?)
- Conjecture synthesis for inductive theories
- Recycling proof patterns in Coq: case studies
- scientific article; zbMATH DE number 1863385 (Why is no real title available?)
- Synthesis of list algorithms by mechanical proving
- Narrowing based inductive proof search
- Deduction as an engineering science
- Plans and planning in mathematical proofs
- Termination orderings for rippling
- A colored version of the -calculus
- Verifying procedural programs via constrained rewriting induction
- The use of embeddings to provide a clean separation of term and annotation for higher order rippling
- Verification by Parallelization of Parametric Code
- Theorem Proving in Higher Order Logics
- Artificial Intelligence and Symbolic Computation
- Case-analysis for rippling and inductive proof
- Extensions to the rippling-out tactic for guiding inductive proofs
- Higher-order annotated terms for proof search
- Automated theorem provers: a practical tool for the working mathematician?
- Quantifier-free induction for lists
- Automating Event-B invariant proofs by rippling and proof patching
- Rippling: A heuristic for guiding inductive proofs
- An integrated approach to high integrity software verification
- A proof-centric approach to mathematical assistants
This page was built for publication: Rippling: Meta-Level Guidance for Mathematical Reasoning
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5462949)
