 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


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 nontrivial 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 LCFarchitecture 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 LCFstyle proof assistant • the mark for the presentation in the third part of the course 
Predicate logic. Basic set theory. Lambda calculus. 
  Required materialsBlackboardThere 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 

 Instructional modesCourse occurrence
 Lecture
 Practical computer training
 Presentation
 Zelfstudie

 TestsTentamenTest weight   1 
Opportunities   Block KW4, Block KW4 


 