The proof theoretic foundation of computational logic

Dale Miller will teach a graduate course at the University of Pisa during 10-17 April 2014. Most classes will be in Sala Seminari Est from 11-13h.

Abstract: I will present proof theory in the Gentzen/Girard tradition and layer on it recent results on focused proof systems. I will then make systematic use of that framework to present (1) flexible proof systems for classical, intuitionistic, and linear logics; (2) a foundation for a range of computational logic tools, ranging from logic programming, theorem proving, and model checking; and (3) recent work on defining a general approach to proof certificates.

Prerequisites: A 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 planned. For those who would like to explore a bit of coding related to the lectures, please contact the instructor.

Course evaluation: Evaluation of this class involves writing a report based on one of three projects.

Lecture 1, April 10: We present a single, formal framework for presenting a number of topics in computational logic. This framework is based on formal devices introduced in the first half of the last century. In particular, we shall use the Church's treatment of terms and formulas found in his Simple Theory of Types (STT) and Gentzen's presentation of proof using sequent calculus. Various elements of Girard's linear logic are also introduced. Read chapters 2, 3, and 4 (pages 7 - 28) of the lecture notes Sequent calculus and proof search. Try several of the exercises listed there. The paper Finding Unity in Computational Logic provides a background and overview of the topics covered in these lectures.

Lecture 2, April 11: Overview of the sequent calculus for classical and intuitionistic logics. Slides.

Lecture 3, April 14: Restart rule. Cut-elimination and its consequences. How to structure the search for cut-free proofs. Slides.

Lecture 4, April 15: The LKF focused sequent calculus. Applications of LKF to proof certificates. Proof of Herbrand's theorem. Handout. Slides.

Lecture 5, April 16: Presenting term equality. Unfolding of fixed points. Induction and coinduction. A (focused) proof theory for Peano Arithmetic. Handout. Slides.

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