A BRICS Mini-Course
August 11, 1994
Max-Planck-Institut für Informatik, Saarbrücken, Germany
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 some of the central issues in automating proof by mathematical induction will be covered. 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.