The proof assistant course consists of three parts:
In this part of the course the Mizar proof assistant is taught from the user perspective. Specific aspects of Mizar are:
The version of Mizar used in the course is Mizar version 7.11.01 (or for Windows).
In this part of the course the HOL Light proof assistant is taught from the implementer perspective. Specific aspects of HOL are:
The version of HOL used in the course is the snapshot of HOL Light of 23rd January 2009.
In this part of the course proof assistants different from Mizar, HOL and Coq will be presented.
For each part of the course a grade will be given. The final grade of the course will be the average of those three grades. The first two parts both have an exercise: doing a formalization and implementing a small proof assistant. For the third part a presentation of a proof assistant different from Mizar, HOL and Coq has to be given.
Here is the schedule of the course:
| February 13 | 02.508 | Introduction | introduction slides, QED manifesto |
| February 20 | 02.032 | Mizar: 1.1-1.3 | Mizar tutorial |
| February 27 | no meeting | ||
| March 6 | no meeting | ||
| March 13 | 02.032 | Mizar: 1.4-1.5 | Mizar exercise |
| March 20 | 00.065 | Mizar: 1.6-1.8 | "by" paper |
| March 27 | 00.065 | Mizar: 2.1-2.3 | |
| April 03 | 00.065 | Systems: overview | seventeen provers |
| April 10 | no meeting | ||
| April 17 | 01.057 | HOL: logic | HOL manual, HOL logic chapter, HOL exercise |
| April 24 | 00.065 | HOL: kernel | hol.ml, fusion.ml, bool.ml |
| May 1 | no meeting | ||
| May 8 | no meeting | ||
| May 15 | 00.065 | HOL: goals, tactics | HOL reference, tactics.ml |
| May 22 | no meeting | ||
| May 29 | 00.065 | HOL: conversions, rewriting | equal.ml, drule.ml, simp.ml |
| June 5 | 00.065 | HOL: decision procedures | model elimination |
| June 12 | 00.065 | Systems: presentations | |
| 13:45-14:30 14:45-15:30 | Systems: PhoX Systems: B method | Vincent Bettoni: files Serge Mbitom: files | |
| June 19 | 00.065 | Systems: presentations | |
| 13:45-14:30 14:45-15:30 | Systems: Agda Systems: Epigram | Flavien Audin Bertrand Vidal: files | |
| June 26 | 00.065 | Systems: presentations | |
| 13:45-14:30 14:45-15:30 | Systems: Metamath Systems: ssreflect | Nadya Kalabishka: file Robbert Krebbers: file1, file2 |
This schedule might be changed if necessary.
Related to the required work of the course there are several dates. Each of the two exercises has a start date, a "halfway point" date, and a deadline. The schedule for this is:
| March 18 | Mizar exercise: handed out |
| April 17 | Systems: system for presentation selected |
| April 17 | HOL exercise: handed out |
| April 24 | Mizar exercise: halfway point |
| May 29 | HOL exercise: halfway point |
| June 12 | Mizar exercise: deadline |
| June 26 | HOL exercise: deadline |