Difference matching

MaRDI QIDQ4264732zbMATH OpenFDO

Authors Toby Walsh, David Basin

Publication date 10 October 1999

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Rippling: A heuristic for guiding inductive proofs
• A calculus for and termination of rippling

Cited in

(11)

• A recursion planning analysis of inductive completion
• Appropriate lemmae discovery
• Productive use of failure in inductive proof
• Smart matching
• scientific article; zbMATH DE number 1305486 (Why is no real title available?)
• Lemma discovery in automating induction
• A divergence critic
• Using a generalisation critic to find bisimulations for coinductive proofs
• Inverse Unfold Problem and Its Heuristic Solving
• Verifying procedural programs via constrained rewriting induction
• Rippling: A heuristic for guiding inductive proofs

This page was built for publication: Difference matching

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