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 |
|