Case-analysis for rippling and inductive proof

DOI10.1007/978-3-642-14052-5_21zbMATH Open1291.68352OpenAlexW1541587797MaRDI QIDQ5747656FDOQ5747656

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

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

Mathematics Subject Classification ID

Cited In (10)

• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Model Finding for Recursive Functions in SMT
• Automating Induction with an SMT Solver
• Extensions to the rippling-out tactic for guiding inductive proofs
• Title not available (Why is that?)
• Symbolic automatic relations and their applications to SMT and CHC solving
• The automation of proof by mathematical induction
• TIP: Tons of Inductive Problems
• Theory exploration powered by deductive synthesis
• Removing algebraic data types from constrained Horn clauses using difference predicates

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)