Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery

DOI10.1007/978-3-642-17172-7_6zbMath1309.68169OpenAlexW2098766316MaRDI QIDQ3058453

Alan Bundy, Lucas Dixon, Moa Johansson

Publication date: 22 November 2010

Published in: Verification, Induction, Termination Analysis (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/1842/4770

Mathematics Subject Classification ID

Uses Software

• Isabelle
• Theorema
• Isabelle/HOL
• IsaPlanner
• IsaCoSy

Cites Work

• Unnamed Item
• Conjecture synthesis for inductive theories
• Experiments with proof plans for induction
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Isabelle/HOL. A proof assistant for higher-order logic
• Productive use of failure in inductive proof
• Middle-out reasoning for synthesis and induction
• A calculus for and termination of rippling
• Improvements in Formula Generalization
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Theorem Proving in Higher Order Logics

This page was built for publication: Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery