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