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.05 (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 10th January 2010.
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 3 | Introduction | QED manifesto |
| February 10 | Mizar: 1.1-1.3 | |
| February 17 | vacation | |
| February 24 | Mizar: 1.4-1.5 | |
| March 3 | no lecture | |
| March 10 | Mizar: 1.6-1.8 | Mizar exercise |
| March 17 | no lecture | |
| March 24* | Mizar: 2.1-2.3 | |
| March 31 | Systems: overview | |
| April 7 | quarter break | |
| April 14 | quarter break | |
| April 21 | HOL: logic | HOL manual HOL logic chapter HOL exercise |
| April 28 | HOL: kernel | hol.ml fusion.ml equal.ml bool.ml |
| May 5 | vacation | |
| May 12 | HOL: goals, tactics | HOL reference tactics.ml |
| May 19 | HOL: conversions, rewriting | drule.ml simp.ml |
| May 26 | HOL: decision procedures | model elimination |
| June 2 | Systems: presentations Bob van der Linden: PVS Carst Tankink: B method | slides slides |
| June 9 | Marc Schoolderman: ACL2 James McKinna: Epigram | slides examples: 1 2 slides examples: 1 2 3 |
| June 16 | Boy Boshoven: Isabelle | slides |
*Because of Thalia symposium "Formal Methods" on March 24 from 10:45 to 12:30 in HG01.028.
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 10 | Mizar exercise: handed out |
| March 31 | Mizar exercise: halfway point |
| April 21 | Systems: system for presentation selected |
| April 21 | HOL exercise: handed out |
| May 26 | HOL exercise: halfway point |
| June 29 | Mizar exercise: deadline |
| June 29 | HOL exercise: deadline |