Case-analysis for rippling and inductive proof

DOI10.1007/978-3-642-14052-5_21MaRDI QIDQ5747656zbMATHOpenAlexFDO

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

(10)

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

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)