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.
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].
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
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].
the proof theory of regular fixed points, TABLEAUX'09, February 2009.
David Baelde and Dale Miller
and greatest fixed points in linear logic, LPAR 2007: Logic for
Programming Artificial Intelligence and Reasoning.
David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu.
Bedwyr system for model checking over syntactic expressions, CADE
2007, LNAI 4603, pages 391-397. Springer, 2007.
- E. Allen Emerson, The Beginning
of Model Checking: A Personal Perspective.
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.
Radha Jagadeesan, Gopalan Nadathur, Vijay A. Saraswat:
Concurrent Systems: An Interpretation of Intuitionistic
Logic. FSTTCS 2005: 517-528.
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.
- 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.