Handbook of Automated Reasoning

Chapter 13

The Automation of Proof by Mathematical Induction

Alan Bundy

Contents

1  Introduction   847

1.1 Explicit vs Implicit Induction   848

1.2 Conventions   848

2 Induction Rules   848

2.1 Nœtherian Induction   849

2.2 Constructor vs Destructor Style Induction Rules   849

2.3 Additional Universal Variables   850

3 Recursive Definitions and Datatypes   851

3.1 Recursive Datatypes   851

3.2 Recursive Definitions   852

3.3 Recursion/Induction Duality   854

3.4 The Need for Induction   854

4 Inductive Proof Techniques   855

4.1 Rewriting   855

4.2 Fertilization   858

4.3 Destructor Elimination   860

4.4 Termination of Rewriting   862

4.5 Decision Procedures   862

5 Theoretical Limitations of Inductive Inference  ...