Dates: 21st and 22nd of Nov
This is a two day course for students at the ITU University of Copenhagen. It provides a foundation in the field of proof planning and introduces techniques for the automation of inductive Proof. In particular, rippling and proof critics are presented. These guide the search for a proof and patch failed proof attempts. Patches include revisions to the choice of induction rule, the introduction of intermediate lemmata and the generalisation of inductive formulae.
This is for:
Students of the PLS, SDG, and CLA groups.
This course is now finished, so it is too late to sign up.
Outline for study:
Related Reading Material:
An Introductory Article -- a gentle and fun introduction to the inductive proof by Alan Bundy
A Science of Reasoning -- on proof planning, by Alan Bundy
The Automation Of Proof By Mathematical Induction -- by Alan Bundy
The Rippling book. -- This is a comprehensive discussion and presentation of rippling for first order theories. By Alan Bundy, David Basin, Dieter Hutter, Andrew Ireland.
Higher Order Rippling in IsaPlanner -- by Lucas Dixon and Jacques Fleuriot