Proof Theory Seminar
MPISWS/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
cutelimination. The course will cover the proof theory of
different propositional and firstorder variants of many logics,
e.g., intuitionistic logic, classical logic and modal logic.
Prerequisites
No formal prerequisites, but we will assume some familiarity
with rigorous proof techniques such as structural induction.
Organization
Open to all members of UdS, MPISWS, MPIInformatik and
TUKL. 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 fpatp 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 reattempts 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 reattempts 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 
fpatp, chapter 2 
April 19 
Natural deduction, part 2 
Assignment 1 out [PDF]
fpatp, chapter 2

April 23 
Proof terms and CurryHoward isomorphism 
fpatp, chapter 2

April 26 
Sequent calculus 
fpatp, chapter 3.3

April 30 
Admissibility of cut 
Assignment 1 due before class
fpatp, chapter 3.4

May 3 
Canonical proofs in natural deduction and identity theorem 
Assignment 2 out [PDF]
fpatp, chapters 3.1, 3.3

May 7 
Classical logic 
fpatp, chapter 3.7
[Wadler03] (Extra reading)
[Griffin90] (Extra reading)

May 10 
Kolmogrov's double negation translation and Glivenko's Theorem 
fpatp, chapter 3.7
[Griffin90], Section 6 (Extra reading)
[Wadler03], Section 6 (Extra reading)
[FerreiraOliva10], Section 1 (Extra reading)

May 14 
Firstorder logic 
Assignment 2 due
fpatp, pp. 1214, 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 MPISWS 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 
Tableaubased decision procedures (Ruzica Piskac) 

July 19 
Tableaubased decision procedures (Ruzica Piskac) 
Assignment 5 due
All redo assignments due

July 23 
Focused Proof Search 
