A graduate course:
Proof systems for linear, intuitionistic, and classical logic
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
- 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
Focusing and Polarization in
Sequent calculus for classical and intuitionistic logics. Basic
results about uniform proof. A
proof theory foundation for logic programming.
Sequent calculus for linear logic. Generalize uniform proof and
show new possibilities for logic programming.
Focused proof systems for linear, intuitionistic, and classical
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.
Two recent papers that provide flexible focused proof systems for
intuitionistic and classical proof systems. A conference
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).
- 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.
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.
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
Di Cosmo and Dale Miller. The Stanford
Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (ed.).