Induction Based on Rippling and Proof Planning.
David A. Basin
Mathematical Induction is a central technique in reasoning about programs and their properties, e.g., loops and recursion, recursively defined data-structures, and program termination. For researchers interested in establishing these properties on a computer, such reasoning must be automated or at least partially supported. In this five hour seminar I will cover some of the central issues in automating proof by mathematical induction. In particular, formalisms for mathematical induction, techniques for selecting induction schemata and well-founded orders, rewriting in inductive theorem proving, and applications. The topics will often be illustrated using ideas and techniques that have been developed at Edinburgh and embodied in the CLAM Inductive Theorem Proving System.
Available as PDF.