| |
Courses - 2IF40
Last update:
November 27th, 2006
Course: Proving with Computer Assistance
Code: 2IF40
Dutch name: Bewijzen met Computer Ondersteuning
ECTS Points: 2.9
For: INF-4.2
Duration: Course of two hours per week, during nine weeks.
Teachers: Dr. F. Dechesne, A. Koprowski.
Written examination: Dr. R. P. Nederpelt.
Questions:
Francien Dechesne: HG 7.17, tel: 040-2475025, f.dechesne@tue.nl
Adam Koprowski: HG 6.78, tel: 040-2472993, a.koprowski@tue.nl
Rob Nederpelt: Monday afternoon, 15:30 - 16:00, HG 7.20, tel: 040-2472718,
r.p.nederpelt@tue.nl.
Aim:
The aim of this course is to give insight in the background
of so-called `theorem provers'. A theorem prover is a computer tool which
assists the user in proving the correctness of mathematical theorems and
of computer programs. Theorem provers are also used as interactive tools
for the development of mathematical theories and correct programs.
Course material:
Will be distributed during the course:
(1) Rob Nederpelt, Theorem Provers, November 2005, 5 pages.
(2) Rob Nederpelt, Basics of Type Theory, Chapters 1 to 7, draft version, 23th November 2005, 130 pages.
more information:
(A) 2IF44: Course Notes of the theoretical part (from academic year 2004/5) can be found at
http://ledr.luon.net/courses/2IF40/.
Note: There are minor differences with the present course.
(B) 2IF48: The information for the practical part of this course is made available at http://www.win.tue.nl/~akoprows/teaching/Coq/.
Examination:
2000/2001: assignment.
2001/2002, 2002/2003, 2003/2004, 2004/2005, 2005/2006, 2006/2007:
(A) Written examination 2IF44 about the theory, plus
(B) Assignment 2IF48 (contact A. Koprowski).
The written examination (A) takes three hours. It is an 'open
book' examination, which means that the student may use written material
that he/she brings along.
The assignment (B) should be finished ultimately on .
Assessment:
The final grade for 2IF40 is the average of the grades obtained for
2IF44 (Part A) and 2IF48 (Part B), on the condition that the
grades are both `satisfactory' (i.e, 6 or more on a scale of 10).
Contents:
The first six weeks (lecturer: F. Dechesne) will be used to give the necessary background
knowledge in order to understand the principles behind theorem provers.
The theoretical frame for this is called Type Theory.
In the final three
weeks (lecturer: A. Koprowski), practical tools will be presented (Coq and PVS). Moreover, the
student gets the opportunity to work with one of these tools by doing
exercises in a lab session (week 8).
Week 1: Introduction. Lambda calculus (type-free), terms, reduction,
confluence, normalisation.
Week 2: Types. Simply typed lambda calculus: lambda-arrow-Church.
Week 3: Properties of lambda-arrow. Polymorphism. Lambda-2.
Week 4: Pi-types. Lambda-omega-bar.
Week 5: Lambda-P. Predicates. Logic in lambda-P.
Week 6: Lambda-C. Properties of lambda-C. The coding of mathematics
in Type Theory: sets, axioms, definitions, theorems, proofs.
Week 7: Introduction in working with the theorem prover Coq.
Week 8: Exercises with Coq (computer lab session).
Week 9: Introduction to PVS.
Old examinations:
The following texts of the examinations of the theoretical Part A,
2IF44 (formerly 2R844), are available, in pdf-version and in postscript-version,
respectively
(Dutch versions)
(English versions)
| March
26, 2002, pdf |
March
26, 2002, postscript |
| May 13, 2002,
pdf |
May 13, 2002,
postscript |
| March 20, 2003,
pdf |
March 20, 2003,
postscript |
| May 12, 2003, pdf |
May 12, 2003, postscript |
| March 10, 2004, pdf |
March 10, 2004, postscript |
| May 11, 2004, pdf |
May 11, 2004, postscript |
| March 16, 2005, pdf |
March 16, 2005, postscript |
| April 28, 2005, pdf |
April 28, 2005, postscript |
| March 15, 2006, pdf |
March 15, 2006, postscript |
| May 8, 2006, pdf |
May 8, 2006, postscript |
Solutions:
answers to
the examination of March 20th, 2003, pdf
answers to the
examination of March 20th, 2003, postscript
|
