Structural and Computational Proof Theory

This project is a consortium of four partners, two French and two Austrian, all being internationally recognized for their work on structural proof theory, but each coming from a different tradition. One of the objectives of the project is to build a bridge between these traditions in order to develop new tools and techniques for structural proof theory. These will have a large potential for applications in computer science, in particular at the level of models of computation, and the extraction of programs and effective bounds from proofs. On one side, the project partners represent the tradition coming from mathematics, which is mainly concerned with first-order logic, and studies, e.g., Herbrand`s theorem, Hilbert`s epsilon calculus, and Goedel`s Dialectica interpretation. On the other side, the partners represent the tradition coming from computer science, which is mainly concerned with propositional systems, and studies, e.g., Curry-Howard isomorphism, algebraic semantics, linear logic, proof nets, and deep inference. A common ground of both traditions is the paramount role played by analytic proofs and the notion of cut elimination. We will study the inter-connections of these different traditions, in particular we focus on different aspects and developments in deep inference, the Curry-Howard correspondence, term-rewriting, and Hilbert`s epsilon calculus. As a byproduct this project will yield a mutual exchange between the two communities starting from this common ground, and investigate, for example, the relationship between Herbrand expansions and the computational interpretations of proofs, or the impact of the epsilon calculus on proof complexity. Besides the old, but not fully exploited, tools of proof theory, like the epsilon calculus or Dialectica interpretation, the main tool for our research will be deep inference. Deep inference means that inference rules are allowed to modify formulas deep inside an arbitrary context. This change in the application of inference rules has drastic effects on the most basic proof theoretical properties of the systems, like cut elimination. Thus, much of the early research on deep inference went into reestablishing these fundamental results of logical systems. Now, deep inference is a mature paradigm, and enough theoretical tools are available to think to applications. Deep inference provides new properties, not available in shallow deduction systems, namely full symmetry and atomicity, which open new possibilities at the computing level that we also intend to investigate in this project. We intend to investigate the precise relation between deep inference and term rewriting, and hope to develop a general theory of analytic calculi in deep inference.

Structural and Computational Proof Theory The aim of the STRUCTURAL project can be summarised as follows:Structural and Computational Proof Theory investigates the fine structure of formal proofs inan algorithmic manner.The STRUCTURAL project has been concerned with understanding the computational content of proofs, extracting programs from proofs and improving programming practices by refining logical control over computational operations. It is carried out by a consortium of four partners, two Austrian and two French, all being internationally recognised for their work on structural proof theory, but each coming from a different tradition. The spirit of the project is to apply the powerful and promising techniques from structural proof theory - in particular deep inference, Herbrand disjunctions, and Hilbert's ?-calculus - to problems in computer science for which they have not been used before, in particular in the realm of programming languages. The approach can be described in two ways, which are the two sides of the correspondence between proofs and programs, called Curry-Howard correspondence: if one looks from the computer science side, it is to type with logical systems computational operations that one doesn't know how to type yet; if one looks from the logical side, it is to to find new computational interpretations of proof systems, which might correspond to computational models which are already used in practice or completely new ones. The common background idea of the approach is to overcome the limitations of traditional logical systems, for example in the analysis of programming languages, by introducing symmetry and atomicity properties and by reducing quantifiers to terms.Main results The combined expertise of the teams led remarkable progress in three main themes of the project, opening new fields of research of major interest. It has been shown, for instance, that computational interpretations of deep inference can provide an adequate typing of ?-calculus with explicit sharing and of interaction nets. It has also been shown that, surprisingly, the non determinism of the computational interpretations of classical logic can be controlled by Herbrand formulas. Furthermore a novel characterisation of finitely-valued Gödel logics could be given with the help of Hilbert's ?-calculus.Factual information The STRUCTURAL project was an international basic research project coordinated by Michel Parigot (PPS Laboratory, University Paris-Diderot). It brings together teams of the University of Innsbruck, the Vienna University of Technology, INRIA Saclay, and the University Paris-Diderot. The Austrian side of the project has been coordinated by Georg Moser (University of Innsbruck). The project started on February, 1 2011 and lasted 38 months. It benefited from an FWF funding of 314.000,-.