Duration: 12 months
Starting date: Between 1 Feb 2013 and 1 Apr 2013
Working place: École
Polytechnique, LIX
Structural and Computational Proof Theory
The postdoc position is financed by the
ANR project STRUCTURAL, whose objective
is to investigate the structural and 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 STRUCTURAL project.
The main task of the successful candidate will be to support the
research effort towards the goals expressed in the scientific program
of
the STRUCTURAL
project description 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
related fields.
Applicants should send their application, including CV, research statement (1-2 pages) and one or two recommendation
letters to Lutz
Straßburger.
Deadline: 31 January 2013