Proof Theory Seminar

MPI-SWS/University des Saarlandes
Summer 2012

Campus E1 5 Room 029 (Video link to KL 206)
Monday, Thursday
15:30 - 17:00

Instructor: Deepak Garg
Teaching Assistant: Beta Ziliani

Overview

We will explore fundamental topics in proof theory including natural deduction, sequent calculi, structural properties of proof systems, proof terms, proof normalization and cut-elimination. The course will cover the proof theory of different propositional and first-order variants of many logics, e.g., intuitionistic logic, classical logic and modal logic.

Pre-requisites

No formal pre-requisites, but we will assume some familiarity with rigorous proof techniques such as structural induction.

Organization

Open to all members of UdS, MPI-SWS, MPI-Informatik and TU-KL. Students interested in UdS credits will be evaluated through periodic assignments and a final exam. Everyone is welcome to complete the assignments.

Initial meetings will be organized as lectures by the instructor. Later topics may be presented by other participants.

The language of this seminar is English.

Notes and lectures

Past lectures can be viewed here with the username and password provided in class. Notes and references will be provided to the extent possible and linked from the schedule below. For some lectures, we will use Frank Pfenning's notes on Automated Theorem Proving (called fp-atp in the sequel). These notes can be found here or locally mirrored here.

Homework collaboration/resubmit policy

Starting from homework 2, you will be allowed re-attempts on problems (as many as you need) before you obtain solutions that the teaching staff find satisfactory. The intent of this policy is to ensure that you learn, without requiring that you get everything right the first time. You will not receive any points on your solutions, but only a satisfactory (S) or unsatisfactory (U) grade for each problem (or subproblem) along with detailed comments. For problems marked unsatisfactory, you are expected to submit a new solution within one week. This can be repeated till you get the solution right. The only way to not get a satisfactory grade in this grading scheme is to either give up or run out of time at the end of the semester! Note that partial attempts will result in better feedback than no attempts and make re-attempts easier, so you are encouraged to submit partial solutions and/or thoughts when you don't have full solutions.

Also starting from homework 2, verbal collaboration is allowed on homeworks. This means that you can discuss homework problems and their solutions with anyone (including the instructor and people not in the class), but you must not take out any written/electronic material from such discussions. The intent of this policy is to promote collaborative learning, yet ensure that every person reconstructs every solution in its entirety at least once. Discussions over email and searching the Internet for solutions are prohibited.

Schedule

The schedule given below is tentative and will be updated as the class progresses.

Date Topic and Presenter Materials and Assignments
April 16 Natural deduction for intuitionistic logic, part 1 fp-atp, chapter 2
April 19 Natural deduction, part 2 Assignment 1 out [PDF]
fp-atp, chapter 2
April 23 Proof terms and Curry-Howard isomorphism fp-atp, chapter 2
April 26 Sequent calculus fp-atp, chapter 3.3
April 30 Admissibility of cut Assignment 1 due before class
fp-atp, chapter 3.4
May 3 Canonical proofs in natural deduction and identity theorem Assignment 2 out [PDF]
fp-atp, chapters 3.1, 3.3
May 7 Classical logic fp-atp, chapter 3.7
[Wadler03] (Extra reading)
[Griffin90] (Extra reading)
May 10 Kolmogrov's double negation translation and Glivenko's Theorem fp-atp, chapter 3.7
[Griffin90], Section 6 (Extra reading)
[Wadler03], Section 6 (Extra reading)
[Ferreira-Oliva10], Section 1 (Extra reading)
May 14 First-order logic Assignment 2 due
fp-atp, pp. 12-14, 38
May 17 No class (Ascension day) Assignment 3 out [PDF]
May 21 Proof normalization by Tait's method (Derek Dreyer) [Notes by Beta Ziliani]
[Gallier89]
May 24 Proof normalization by Tait's method (Derek Dreyer) [Gallier89]
May 28 No class (Whit Monday) Assignment 3 due on May 29
May 31 Proof Normalization for System F (Derek Dreyer) Proofs and Types, chapters 11, 15 (Extra reading)
[HM99] (Extra reading)
June 4 Semantics of classical logic Assignment 4 out [PDF]
June 7 No class (Corpus Christi and MPI-SWS retreat)  
June 11 Semantics of classical logic  
June 14 No class (TaPP)  
June 18 Kripke semantics of intuitionistic logic Assignment 4 due
June 21 Kripke semantics of intuitionistic logic  
June 25 No class (CSF)  
June 28 No class (CSF)  
July 2 Intuitionistic Linear Logic (Multiplicative fragment)  
July 5 Intuitionistic Linear Logic (Exponential)  
July 9 Intuitionistic Linear Logic (Additives)  
July 12 Inversion and weak focusing Assignment 5 out [PDF]
July 16 Tableau-based decision procedures (Ruzica Piskac)  
July 19 Tableau-based decision procedures (Ruzica Piskac) Assignment 5 due
All re-do assignments due
July 23 Focused Proof Search