Zoek
English
  Studiegidsen 2008-2009
Radboud UniversiteitStudiegidsenFaculteit der Natuurwetenschappen, Wiskunde en Informatica > Master Computing Science

Proof Assistants 

(Vakcode)
Course ID
I00139
(Studiepunten)
Credits
6
(Periode)
Scheduled
tweede semester
Introduction (Inleiding)
This course is an introduction to proof assistants. A proof assistant is a program in which one can encode a mathematical proof (which often is a proof in which software or hardware is proved correct) in such a way that it will be impossible for it to be incorrect, as the computer will check full correctness.

The course both presents all main proof assistants, and also teaches two proof assistants in detail: the Mizar system from Poland, and the HOL system from Cambridge in the UK.

The course focuses on the use of proof assistants for their use in mathematics.

Proof assistants are one of the main subjects studied in the Intelligent Systems research group of the ICIS institute.
Objectives (Leerdoelen)
After the course students can:
  • develop a formalization in a proof assistant
  • implement a simple proof assistant
  • select an appropriate proof assistant for a given purpose
  • install and use a proof assistant that they have not seen before

Subjects (Onderwerpen)
  • the Mizar proof assistant
  • the HOL proof assistant
  • the LCF-architecture for proof assistants
  • defining and proving in a proof assistant
  • dependent types and implicit arguments
  • clusters and registrations, redefinitions
  • searching for lemmas in a proof assistant
  • proof automation and decision procedures
  • goals, tactics, tacticals
  • conversions and rewriting
  • applications of proof assistants
Study investment (Studielastverdeling)
  • 30 hrs lecture
  • 30 hrs laboratory course
  • 108 hrs individual study period
Teaching methods (Toelichting werkvormen)
The course has three parts:
  • Mizar: using a proof assistant
  • HOL: implementing a proof assistant
  • overview of the other proof assistants
The first two parts consists of lectures.  During these parts students will be working on exercises during the practicum. There will be a final exercise for each of these two parts, that will have to be handed in.

The third part consists of presentations by the students. Each student will present a different proof assistant. As preparation for this part there is one lecture with an overview of proof assistant, to enable students to make a motivated choice for their presentation.

If there are only a few students, the practicum will not be given as contact hours, but instead there will be regular meetings for feedback.
Examination (Toetsvorm)
The final note will be the average of three marks:
  • the mark for the Mizar formalization
  • the mark for the small LCF-style proof assistant
  • the mark for the presentation in the third part of the course
There is a deadline for handing in the two exercises. If this deadline is not met, the exercise will be considered not to have been made.

Pre-requisites (Vereiste voorkennis)
Predicate logic.  Basic set theory.  Basic lambda calculus.
Literature (Literatuur)
There are various documents that will be used to support the course.  These will be made available on the website in pdf format.

The main of these documents are course notes on the Mizar system by Freek Wiedijk, and the manual of the HOL Light system by John Harrison.
Website
http://www.cs.ru.nl/~freek/courses/pa-2009/
Extra information (Bijzonderheden)
This course is very interesting for mathematics students. This course does not teach the Coq proof assistant, as that is the subject of the Type Theory course.