A graduate course:
Proof systems for linear, intuitionistic, and classical logic

Venue

Dale Miller lectures for 20 hours during the weeks after Easter at the Dipartimento di Informatica, Università Ca' Foscari Venezia.

• 15 April: 10h00 - 13h00. Chapters 1 and 2 of lecture notes.
• 16 April: 10h00 - 13h00. Chapter 3. Exercises to be discussed in class Monday, 20 April: 8, 9, 12 (solution in handout), 18, 19, 21.
• 17 April: No lectures today. Hours have been moved to the following week.
• 20 April: 10h00 - 13h00: Chapter 4 (hc, hh)
• 21 April: 10h00 - 13h00: Chapter 5 (backchaining)
• 22 April: 10h00 - 13h00: Chapter 6 (linear logic)
• 23 April: 10h00 - 13h00: Chapter 6 (linear logic programming)
• 24 April: 11h00 - 13h00: Other topics: Encryption as an abstract data-type and Focusing and Polarization in Intuitionistic Logic.

Topics

1. Sequent calculus for classical and intuitionistic logics. Basic results about uniform proof. A proof theory foundation for logic programming.
2. Sequent calculus for linear logic. Generalize uniform proof and show new possibilities for logic programming.
3. Focused proof systems for linear, intuitionistic, and classical logic.
4. If time permits, applications of focusing proofs will be presented: Herbrand's theorem, model checking, theorem proving with induction and co-induction, etc.

Exam / Evaluation

The exam for the course should be returned to Miller by 15 May 2009.

Five students have taken the exam: Raju Halder, Luca Leonardi, Andrea Petrucci, Andrea Triossi, Matteo Zanioli.

References and Links

Lecture notes are available as pdf. Please have a copy of these available in order to follow the lectures.

Below are some documents available via the web that may be of use in this class.

1. Two recent papers that provide flexible focused proof systems for intuitionistic and classical proof systems. A conference paper (CSL'07): Focusing and Polarization in Intuitionistic Logic by Chuck Liang and Dale Miller (pdf, slides). An extended, journal version of that work: Focusing and Polarization in Linear, Intuitionistic, and Classical Logic by Chuck Liang and Dale Miller. Accepted (March 2008) to TCS. Draft dated May 2008: (pdf).
2. Logic for Computer Science: Foundations of Automatic Theorem Proving, by Jean Gallier, Wiley, pp. 511 (1986). This book is now out of print but available for free download.
3. Proofs and Types by Jean-Yves Girard, Paul Taylor, and Yves Lafont. Cambridge University Press. This book is now available from a number of sources for free download. Try the link above to find locations for downloading.
4. Proof Theory as an Alternative to Model Theory by Dale Miller. Argues that the theory of proofs should also be considered a foundations for the design and justification of logic programming.
5. Linear Logic by Roberto Di Cosmo and Dale Miller. The Stanford Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (ed.).