Proof theory with applications to computation and deduction

A 20 hour graduate course at the University of Pisa taught by Dale Miller.

Venue: 12-24 September 2011 in the Sala Riunioni Ovest. Contact information for Miller: Phone 050 22 13 114, Office number 396.

The goals of the first week (the first 10 hours) are the following:

1. introduce the students to the basics of the sequent calculus,
2. provide some formal results covering the proof-search approach to computation, and
3. present the basics of linear logic and how it can be used to make the logic programming paradigm more expressive.

The second week (the second 10 hours) will expand the role of the sequent calculus from the specification of logic programming computations to the more general settings of model checking and induction.

Most lectures will be 9am-11am daily. However, there will be no class on Friday, 16 September 2011. Instead that class will be moved to 14:00 on Wednesday, 14 September 2011. The following is an approximate schedule for the class. This schedule will be modified as the course progresses.

• Lecture 1: (12 Sept, 9:00) Overview. The basics of the sequent calculus
• Lecture 2: (13 Sept, 9:00) Sequent calculus proofs for classical and intuitionistic logic.
• Lecture 3: (14 Sept, 9:00) Goal-directed proofs, Horn clauses, Hereditary Harrop formulas, limitations of logic programming
• Lecture 4: (14 Sept, 14:00) Linear logic
• Lecture 5: (15 Sept, 9:00) Linear logic programming in Lolli
• Lecture 6: (19 Sept, 9:00) Linear Logic and Forum (finish lecture notes).
• Lecture 7: (20 Sept, 9:00) Introduce LKF, Focused proof systems for classical logic. Handout
• Lecture 8: (21 Sept, 9:00) Proof theory for fixed points and equality. Handout
• Lecture 9: (22 Sept, 9:00) Model checking, games and winning strategies, Bedwyr.
• Lecture 10: (23 Sept, 9:00) Induction and co-induction

Prerequisites: basic background of first-order logic. Familiarity with the sequent calculus is useful but not strictly necessary.

This is not a lab course and no programming tasks are currently planned. For those who would like to explore a bit of coding related to the lectures, please contact the instructor.

Course materials: Links to course material (including some lecture notes) will be posted here as the course progresses.

1. Draft lecture notes titled Proof Search and Computation.
2. Handout on the LKF proof system.
3. Handout on fixed points and equality.

Course evaluation: The instructor has contacted the students by email and has offered them the choice of either taking a written exam or doing a project.

References and additional reading

Students wanting more material related to the background of this class can find additional references below.

• 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. This short article argues that the theory of proofs should also be considered a foundations for the design and justification of logic programming.

• The Development of Proof Theory by Jan von Plato. The Stanford Encyclopedia of Philosophy (2008), Edward N. Zalta (ed.).

• Linear Logic by Roberto Di Cosmo and Dale Miller. The Stanford Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (ed.).

• Least and greatest fixed points in linear logic by David Baelde and Dale Miller. LPAR 2007: Logic for Programming Artificial Intelligence and Reasoning. Extended version.