Proof theory and automated theorem proving 2019/2020 (Official code: 569076)
Organisation
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 rooms yet to be announced.
The time schedule will be
Mondays: 12:00 -- 13:30;
Wednesdays: 11:00 -- 12:30.
For the first seven weeks,
Tuesdays: 9:00 -- 10:00;
Wednesdays: 11:00 -- 13:00.
For the last seven weeks. The last seven weeks are in Room 409.
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 exams. 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.
We will start Monday, September the 16th. The first seven weeks will be taught by Juan Carlos Martínez Alonso and the last seven weeks by Joost J. Joosten.
THE REMAINDER OF THIS PAGE WILL BE UPDATED SHORTLY
16/9 through 20/9.
Juan Carlos starts the course on Monday.
23/9 through 27/09.
30/09 - 4/10
7/10 - 11/10
14/10 -- 18/10.
21/10 -- 25/10.
28/10 through 01/11.
04/11-08/11
11/11 -- 15/11.
Juan Carlos will have his midterm exam on Monday, November 11.
Joost will start teaching on Wednesday, November 13.
General intro and context, some history.
18/11--22/11.
G3 system, both classical and intuitionistic. Completeness for propositional logic.
25/11 --29/11: no class, homework consists of Exercises 0.1, 0.4, 0.5 and 0.6 from the first homework set
02/12 -- 06/12
09/12 -- 13/12
16/12 -- 20/12
Some time January
Some time January
Question and answer
Question
Q:
Answer
A.:
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.
Question
Q
Answer
A.