Proof theory and automated theorem proving (Official code: 569076)
Lecturers: Joost J. Joosten (for the last two-and-a-half credits) and Juan Carlos Martinez Alonso (for the first two-and-a-half credits)
A course of 5 credits corresponds to 42 contact hours. Since we do three hours a week, this will correspond to 14 weeks.
The lectures will take place in Room 412 at the philosophy department/faculty at Montalegre.
Wednesdays: 15:00 -- 16:30;
Thursdays: 12:30 -- 14:00.
The course consist of two parts of equal weight. The first part is on automated theorem proving and is given by prof. Juan Carlos Martinez Alonso. The second part focuses on the more theoretical part of Proof Theory and is given by Joost J. Joosten. The final grade is determined by the average of the grades obtained for the two respective parts. Homework consists of 25 % of the grade and 75 % of the grade is constituted by a final exam. There will be a final exam (mid-term) in the middle of the course for the Automated Theorem proving part, and a final exam for the Proof Theory part of the course at the end.
All materials and assignments will also be placed on this page.
As mentioned, the lecturers are Joost J. Joosten and Juan Carlos Martinez Alonso. The best way to contact one of us is by sending us a mail. You can also come around to see if we're in. Joost is in the Montalegre building in Room 4045 with phone number +34 934031939. Juan Carlos has telephone number 934021661 and his office is located in the Faculty of Mathematics (Gran Via 585). Here is a link to the official course description.
14/9 through 18/9.
21/9 through 25/9.
Here is a first list of exercises.
28/9 through 2/10.
Here is a second list of exercises.
5/10 through 9/10.
Here is a third list of exercises.
12/10 through 16/10.
Here is a fourth list of exercises.
19/10 through 23/10.
26/10 through 30/10.
2/11 through 6/11.
Free. (Exam on Prolog)
Here is the exam plus answer-set.
9/11 through 13/11.
Joost will start teaching: we did the first part of the book up to Exercise 2.3. The homework consists of giving a formal derivation for the type assignment.
We work from the book "Interactive Theorem Proving and Program Development" from Yves Bertot and Pierre Castéran.
16/11 through 20/11.
We have worked our way through to 2.4 which we just started a bit. We have done various exercises.
23/11 through 27/11.
We finished Chapter 2 and started Chapter 3 as well as lab sessions.
30/11 through 4/12.
We made it to Section 3.4. Homework consists of Exercise 3.2 of the book. Comment your sessions if you deem that appropriate.
7/12 through 11/12.
14/12 through 18/12.
Here it is:
You are asked to make and hand in 6.15; 17 and 18 on Page 166 from the book and have till February 5 for that. Please do duly annotate your answer set to explain what your are doing.
Eduardo has written a short set of examples that might be helpful.
Question and answer