Lucas Dixon → Proof Planning for Inductive Theories

Proof Planning for Inductive Theories

Lecturer: Lucas Dixon

Dates: 21st and 22nd of Nov

Abstract:

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.

Credits: 2.5

Sign up:

This course is now finished, so it is too late to sign up.

Lecture Slides:

You can download the lecture slides 1 per page or 4 per page.

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