Automation of Mathematical Induction as part of the History of Logic

Abstract

We review the history of the automation of mathematical induction

ii+107 pages

References in corpus (5)

• lim+, delta+, and Non-Permutability of beta-Steps
• Syntactic Confluence Criteria for Positive/Negative-Conditional Term Rewriting Systems
• A Simplified and Improved Free-Variable Framework for Hilbert's epsilon as an Operator of Indefinite Committed Choice
• Progress in Computer-Assisted Inductive Theorem Proving by Human-Orientedness and Descente Infinie?
• A Self-Contained and Easily Accessible Discussion of the Method of Descente Infinie and Fermat's Only Explicitly Known Proof by Descente Infinie

Cited by in corpus (1)

• The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions