I00139 (I00139)
Proof Assistants*
< 2006/2007 > 05-02-2007 t/m 01-07-2007 () L
Informatica - Master variant C (2003) Thematische specialisatie Foundations of computer science (6 ec) Keuze informatica (6 ec)
Informatica - Master variant E (2003) Keuze informatica (6 ec)
Informatica - Master variant MT (2005) Thematische specialisatie Foundations of computer science (6 ec) Foundations of computer science (6 ec) Keuze informatica (6 ec) (6 ec) (6 ec)
Informatica - Master variant O (2003) Thematische specialisatie Foundations of computer science (6 ec)
Informatica - Master variant O (2005) Thematische specialisatie Foundations of computer science (6 ec) Keuze informatica (6 ec)
Informatica - Master na HBO Artificial Intelligence variant MT (2004) Keuze informatica (6 ec)
Informatica - Master na HBO Artificial Intelligence variant O (2004) Keuze informatica (6 ec)
Informatica - Master na HBO Computer Security variant MT (2003) Keuze informatica (6 ec)
Informatica - Master na HBO Computer Security variant O (2004) Keuze informatica (6 ec)
Informatica - Master na HBO Embedded Systems variant MT (2003) Keuze informatica (6 ec)
Informatica - Master na HBO Embedded Systems variant O (2004) Keuze informatica (6 ec)
Informatica - Master na HBO Information Systems variant MT (2003) Keuze informatica (6 ec)
Informatica - Master na HBO Information Systems variant O (2004) Keuze informatica (6 ec)
Informatica - Master na HBO Software Construction variant MT (2003) Keuze informatica (6 ec)
Informatica - Master na HBO Software Construction variant O (2004) Keuze informatica (6 ec)
omvang
6 ec (168 uur) : 60 uur plenair college, 0 uur groepsgewijs college, 0 uur computerpracticum, 0 uur 'droog' practicum, 0 uur gesprekken met de docent, 0 uur onderling overleg met medestudenten (werkgroepen, projectwerk e.d.), 108 uur zelfstudie
investering
6 ec * 28 u/ec + #std * (1 + 6ec * 0.15 u/student/ec)
inzet tentatief

examinator
afdeling
tijdbesteding

dr. Freek Wiedijk
sws
185u.

speciale web-site
/~freek/courses/pa-2007/

 

The course Proof Assistants treats the implementation and use of proof assistants like Coq, PVS, HOL en Mizar. In the first part, we present the LCF-approach towards implementing proof assistants and show some decision procedures and how they are implemented. In the second part we show how mathematical proofs are formalized in practice.

Leerdoelen

Understand the general principles behind the implementation of proof assistants and to be able to use them to implement simple decision procedures. Obtain an overview of the different proof assistants that are used, how they differ and what their respective strengths are. Obtain enough experience with at least one of the systems to be able to do a theory and proof development in it.

Onderwerpen

  • Implementation of Proof assistants
  • LCF-approach
  • Procedural and Declarative proof styles
  • Tactics
  • Decision procedures (Automated search in first-order logic Reasoning with equality by congruence closures and rewriting techniques)
  • Proof objects
  • Coq, PVS, HOL, Mizar
  • Formalizing Mathematics

Werkvormen

Lectures and Exercise classes

Vereiste voorkennis

Logic, Semantics, Functional Programming, Basic Mathematics courses.

Tentaminering

Each student will do a few small projects. At the end a group presentation has to be given.

Literatuur

Selected Chapters from "Introduction to Logic and Automated Theorem Proving" by John Harrison. This book has not yet appeared. If necessary, printed copies will be handed out at the lectures. Course Notes.


Evaluatie: studentenquêtes ; geen docentevaluatie bekend Rendement: 10 begonnen, echt meegedaan, geslaagd met 1e kans, geslaagd totaal
Q: