Proof theory and automated theorem proving 2017 (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 a room yet to be announced but most likely at the philosophy department/faculty at Montalegre.
Tuesdays: 11:00 -- 12:30;
Thursdays: 11:00 -- 12:30.
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 have lectures on Tuesdays and on Thursdays from 11:00 -- 12:30 in Aula 402 at the philosophy department.
We will start Tuesday, September the 19th. The first seven weeks will be taught by Juan Carlos Martínez Alonso and the last seven weeks by Joost J. Joosten. Since the first seven weeks saw quite some fall-out due to all kinds of reason, prof Juan Carlos will continue a bit longer and Joost will start Thursday, 16 November.
THE REMAINDER OF THIS PAGE WILL BE UPDATED SHORTLY
18/9 through 24/9.
Juan Carlos starts the course on Tuesday.
25/9 through 1/10.
Here is a first list of exercises.
2/10 - 8/10
9/10 - 15/10
16/10 through 22/10.
23/10 through 29/10.
Here is a second list of exercises.
30/10 through 5/11.
6/11-12/11
Here is a third list of exercises.
13/11 -- 19/11.
Tuesday, there is a midterm exam.
Here is the worked out exam.
Joost starts his part of the course on Thursday. We did spoke on what Proof Theory in the broader understanding is and why one does it. When entering into detail we saw that a natural deduction proof for Peirce's formula does not satisfy the sub formula property. We will be working from the book Basic Proof Theory from A. S. Troelstra and H. Schwichtenberg.
20/11--26/11.
We have done Section 3.5 of the book. The homework consists of Exercise 3.5.7.A (we refer to the numbering of the Second Edition of the book).
27/11 --3/12: We studied properties of the G3 system, and related it to semantics.
4/12 -- 10/12: We started the proof of cut-elimination for G3c propositional.
11/12 -- 17/12: We finished the proof of cut-elimination and observed sub-formula property with parity (positive/negative occurrences). We started a proof of Interpolation.
18/12 -- 24/12: We finished the proof of Interpolation for G3cp; proved cut-elimination for G3ip, proved the disjunction property (with assumptions) and interpolation for the latter.
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.