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
-
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
logic.
-
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
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).
- 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.
- 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.
- Linear
Logic
by Roberto
Di Cosmo and Dale Miller. The Stanford
Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (ed.).