Finding Unity in Computational Logic

Dale Miller will give six hours of lectures during the ISCL 2011: Third International ALP/GULP Spring School on Computational Logic during the week 10-15 April 2011 at the University Residential Center Bertinoro (Forlì-Cesena), Italy.

Abstract: Computational logic is divided into several different fragments. There is the division between the proof-as-program (functional programming) approach and the proof-search (logic programming) approach to specifying computation. There is the division among computation, model checking, and theorem proving. Even at the level of the description of such technical devices as proofs systems, there is the division among sequent calculus, natural deduction, tableaux, and resolution. In these lectures, I will show how recent results in structural proof theory bring an organization to these topics so that these divisions can be understood as certain choices within a large, flexible framework. That framework involves recent lessons learned from linear logic, focused proofs systems, and the use of fixed points and equality as logical connectives.

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

This is not an 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: There are two documents that are associated directly with these lectures.

[PSC]

Proof Search and Computation: a Monograph is available for download as a pdf file. This is a shorten version of a larger set of lecture notes: in particular, material on linear logic and linear logic programming has been dropped for these lectures. There are a number of exercises in this monograph.

[FPS]

Lecture notes on Focused proof systems for intuitionistic and classical logics will soon be available for download as a pdf file.

Lecture 1

Motivation and Background. Introduction to the sequent calculus. The unifying role played by the sequent calculus. Read the introduction and Chapters 1 and 2 of [PSC]. Slides.

Lecture 2

Sequent calculus proof systems for classical and intuitionistic logics. The meaning of cut-elimination. Structure of proof search. Read Chapter 3 of [PSC]. Slides.

Lecture 3

Abstract logic programming languages, uniform proofs, proofs based on Horn clauses and hereditary Harrop formulas. Read Chapter 4 of [PSC]. Slides.

Lecture 4

Focused proof systems generally. The focused proof systems LJF. Applications to logic programming. Slides.

Lecture 5

The focused proof system for classical logic. Equality as a logical connective. Fixed points as logical connectives. Induction and co-induction. Least and greatest fixed points. Focused proof systems for fixed points. Slides.

Lecture 6

Model checking and inductive theorem proving in the sequent calculus over fixed points. Simulation and winning strategies as focused proofs. 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 (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.