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