|
Induction Based on Rippling and Proof Planning.
Mini-Course David A. Basin August 1994 |
Abstract:
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. |