Projects

The following is a list of possible projects that can be done as part of the evaluation of the graduate course at the University of Pisa taught by Miller in September 2011 titled "Proof theory with applications to computation and deduction". The class notes and handouts are likely to be useful for these projects. Additional references are suggested. Others can be used as needed. In all cases, the result of these projects are reports that should illustrate your understanding, both technical and high-level, of the topics proposed.

1. When Gentzen introduced the sequent calculus, he was trying to get certain results (eg, cut-elimination) for classical and intuitionistic logic. Years later, the sequent calculus has been used to describe something much smaller than all of logic: namely, logic programming. Discuss the general relationship between logic programming and sequent calculus from what you can find in the three papers [MNPS], [JNS], [LM].
2. Read the paper [HM] on the linear logic language Lolli and implement an interpreter for Lolli in Prolog or (better) lambda Prolog. Develop several examples of programs in Lolli. Notice that there is an interpreter for Lolli in Prolog available in the reference below. Feel free to us it and improve it. Experiment with new examples of linear logic programming (not just those available in the link below). Write a report describing the high-level aspects of you implementation and your experience with your example linear logic programs.
3. Discuss the possible relationship between model checking (using, say LTL) and classical logic with fixed points (accompanied by the rule for unfolding fixed points: that is, there is no induction and coinduction rules). Most traditional approaches to model checking are not described in proof theoretic terms. Take some standard, simple model checking problems and show how they can be expressed in the sequent calculus with inference rules for fixed point unfolding (and equality). For a background in model checking, read [Emerson]. For the proof theory of fixed points and equality, read the papers [Baelde], [BM], and [BGMNT].

References

[Baelde]

David Baelde, On the proof theory of regular fixed points, TABLEAUX'09, February 2009.

[BD]

David Baelde and Dale Miller Least and greatest fixed points in linear logic, LPAR 2007: Logic for Programming Artificial Intelligence and Reasoning. Extended version.

[BGMNT]

David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. The Bedwyr system for model checking over syntactic expressions, CADE 2007, LNAI 4603, pages 391-397. Springer, 2007.

[Emerson]

E. Allen Emerson, The Beginning of Model Checking: A Personal Perspective.

[HM]

Joshua Hodas and Dale Miller, Logic Programming in a Fragment of Intuitionistic Linear Logic Journal of Information and Computation, 110(2):327-365, 1 May 1994. Prolog code from this paper is available.

[JNS]

Radha Jagadeesan, Gopalan Nadathur, Vijay A. Saraswat: Testing Concurrent Systems: An Interpretation of Intuitionistic Logic. FSTTCS 2005: 517-528.

[LM]

Chuck Liang and Dale Miller, Focusing and Polarization in Intuitionistic Logic, CSL'07: Computer Science Logic, J. Duparc and T. A. Henzinger, editors, LNCS 4646, pages 451-465.

[MNPS]

Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov, Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, Vol. 51 (1991), 125 - 157.