This project is a grouping of three teams through their common interest for a new approach to proof theory, called deep inference, that has been developed during the last five years. We aim at refining its enormous potential and at applying it to problems related to the foundations of logic and to more practical questions in the algorithmics of deductive systems.

Among the list of theoretical problems there is the fundamental need for a theory of correct identification of proofs, and its corollary, the development of a really general and flexible approach to proof nets. A closely related problem is the extension of the Curry-Howard isomorphism to these new representations. Among the list of more practical problems we will tackle questions of strategy and complexity in proof search, in particular for higher-order systems. These questions are intimately related to how proofs themselves are formulated in these systems, and the obvious relationship between deep inference and well established techniques—like deduction modulo and unification for quantifiers—are subjects that we intend to deepen, given their common grouding in rewriting theory. We also intend to explore the formuation and use of more exotic logical systems, for example non-commutative ones, that have interesting applications, as in linguistics and quantum computing. This is a natural continuation of some of the first results that were obtained in deep inference.

Laboratoire d'Informatique
d'Ecole Polytechnique (LIX)

Responsible: Lutz Straßburger (project coordinator)

Laboratoire Lorrain d'Informatique et ses Applications (LORIA)

Responsible: François Lamarche

Preuves, Programmes, Systèmes (PPS)

Responsible: Michel Parigot

Responsible: Lutz Straßburger (project coordinator)

Laboratoire Lorrain d'Informatique et ses Applications (LORIA)

Responsible: François Lamarche

Preuves, Programmes, Systèmes (PPS)

Responsible: Michel Parigot

Last update: June 18, 2007 Lutz Straßburger