Case-analysis for rippling and inductive proof

DOI10.1007/978-3-642-14052-5_21MaRDI QIDQ5747656zbMATH OpenOpenAlexFDO

Authors Moa Johansson, Lucas Dixon, Alan Bundy

Publication date 14 September 2010

Published in Interactive Theorem Proving (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Recommendations

• Rippling: A heuristic for guiding inductive proofs
• Theorem Proving in Higher Order Logics
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• scientific article; zbMATH DE number 1863385
• Extensions to the rippling-out tactic for guiding inductive proofs

Cited in

(12)

• Removing algebraic data types from constrained Horn clauses using difference predicates
• Symbolic automatic relations and their applications to SMT and CHC solving
• The automation of proof by mathematical induction
• Model finding for recursive functions in SMT
• Automating Induction with an SMT Solver
• TIP: tons of inductive problems
• scientific article; zbMATH DE number 1105197 (Why is no real title available?)
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Extensions to the rippling-out tactic for guiding inductive proofs
• Checking equivalence in a non-strict language
• Lemma discovery and strategies for automated induction
• Theory exploration powered by deductive synthesis

Describes a project that uses

Uses Software

• IsaPlanner

This page was built for publication: Case-analysis for rippling and inductive proof

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5747656)