I00139: Proof Assistants

This year there are not enough students for the course to be given in the normal way. Students are supposed to watch the video recordings of last year, and the "lectures" on Wednesday will each week be a "responsiecollege".


The proof assistant course consists of three parts:

Mizar: using a proof assistant

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.12.01 (or for Windows).

HOL: implementing a proof assistant

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.

Systems: overview of other proof assistants

In this part of the course proof assistants different from Mizar, HOL and Coq will be presented.



Lectures Wednesday: 13.45-15.30, HG00.308


February 1
LSFA talk
QED manifesto
February 8
Mizar: 1.1-1.3
clip clip
Mizar intro
Mizar manual
February 15
Mizar: 1.4-1.5
clip clip
Mizar exercise
exercise starting point
February 22 no lecture
February 29 Mizar: 1.6-1.8 clip clip
March 7 Mizar: 2.1-2.3 clip clip
March 14 Systems: overview clip clip
March 21
HOL: logic
clip clip
HOL manual
HOL logic chapter
HOL exercise
March 28 HOL: kernel clip clip
April 4 quarter break
April 11 quarter break
April 18 HOL: goals, tactics clip clip HOL reference
April 25 HOL: conversions, rewriting clip clip
May 2 no lecture
May 9 HOL: decision procedures clip clip model elimination
Systems: presentations
May 23
Rob Tiemens: B Method
June 6 Roel van Dijk: Agda

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:

February 15 Mizar exercise: handed out
March 14 Mizar exercise: halfway point
March 21 Systems: system for presentation selected
March 21 HOL exercise: handed out
April 18 HOL exercise: halfway point
June 20 Mizar exercise: hard deadline
June 20 HOL exercise: hard deadline


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.