This course is an introduction to the field of proof assistants, also known as proof checkers or interactive theorem provers. These are implementations of logical systems, programs for the development and verification of formal proofs, both for mathematics and for computer science. The course presents the current state of the art in proof assistants, and then teaches two specific proof assistants in detail.
The first of these is the Isabelle system. With this proof assistant we focus on the user perspective, and will develop a non-trivial proof in full detail. The second is the HOL system. With this system we focus on the implementation architecture and automation of the system. Finally an overview of the main current proof assistants is presented, and some of the large efforts in this area that are currently ongoing are reviewed.
Proof assistants, both for mathematics and for computer science, are one of the research topics of the Intelligent Systems group.
|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.
• 24 hours computer course
• 24 hours lecture
• 16 hours student presentation
• 104 hours individual study period
Extra information teaching methods: The course has three parts:
• Isabelle: 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.
|• the Isabelle proof assistant|
• the HOL proof assistant
• the LCF-architecture for proof assistants
• defining and proving in a proof assistant
• advanced type systems for proof assistants
• searching for lemmas in a proof assistant
• proof automation and decision procedures
• goals oriënted proof
• rewriting and more general conversions
• applications of proof assistants
|The final note will be the average of three marks:|
• the mark for the Isabelle formalization
• the mark for the small LCF-style proof assistant
• the mark for the presentation in the third part of the course
|Predicate logic. Basic set theory. Lambda calculus.|