Structural and Computational Proof Theory
The postdoc position is financed by the
ANR project FISP, whose objective is to
investigate the fine structure of formal proof systems and their
computational interpretations. Particular focus is on the
computational proof theory of recent proof formalisms, like deep
inference and proof nets. One of the main goals is to find canonical
proof objects. Traditional proof systems, like sequent calculus,
tableaux, or resolution do not provide canonical proofs. The reason is
that their syntax allows for many irrelevant rule permutation.
Proof nets have been conceived to abstract away from these rule permutation, and thus form a "bureaucracy-free" approach to encoding proofs. But the lack of explicit structure in proof nets makes algorithmic aspects of proofs difficult to describe when the logic reaches a certain expressive power. In other words, they are not suited for proof search. Another approach is the concept of focusing, which allows the design of various normal forms of proof that abstract away from many bureaucratic irrelevances.
Both concepts, proof nets and focusing, have been developped with the sequent calculus in mind. But recent results suggest that they are also suitable for deep inference formalisms, and investigating this possibility is an important part of the FISP project.
The main task of the successful candidate will be to support the
research effort towards the goals expressed in the scientific program
project within the Parsifal team, in particular the
candidate will help in designing new proof systems that on the one
hand provide canonical (i.e., bureaucracy-free) proof objects and, on
the other hand, provide concrete enough structures to support
computations based on proof normalization and on proof search.
The candidate should have a good background in proof theory and
Applicants should send their application, including CV, research statement (1-2 pages) and one or two recommendation
letters to Lutz
Deadline: 16 April 2017