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