Guiding induction proofs

DOI10.1007/3-540-52885-7_85MaRDI QIDQ6488528zbMATH OpenFDO

Authors Dieter Hutter

Publication date 28 April 2023

Full work available at URL https://doi.org/10.1007/3-540-52885-7_85

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Experiments with proof plans for induction
• scientific article; zbMATH DE number 4072439
• The automation of proof by mathematical induction
• Induction using term orders
• scientific article; zbMATH DE number 3986670

Cites work

• scientific article; zbMATH DE number 4072439 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 46989 (Why is no real title available?)
• Mechanizing structural induction. II: Strategies

Cited in

(11)

• Productive use of failure in inductive proof
• A calculus for and termination of rippling
• scientific article; zbMATH DE number 6538198 (Why is no real title available?)
• scientific article; zbMATH DE number 2043540 (Why is no real title available?)
• Internal analogy in theorem proving
• Termination of algorithms over non-freely generated data types
• INKA: The next generation
• Lazy generation of induction hypotheses
• Termination orderings for rippling
• A colored version of the -calculus
• Rippling: A heuristic for guiding inductive proofs

This page was built for publication: Guiding induction proofs

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