Canonical proof systems
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. It is an
important research problem to design new proof systems that on the one
hand provide canonical (i.e., bureaucracy-free) proof objects, and on
the other hand provide a rich enough structure for performing proof
The main task of the successful candidate will be to support the
recent research effort within the Parsifal team, in particular the
work on focused proofs and proof nets. Concurrently, members of
Parsifal have been pushing the notion of "focused proof" to its limit
and obtained a "maximally multi-focused" proof system, which yields
canonical proof objects for multiplicative additive linear logic
without units. It is now important to exhibit the precise relation to
proof nets and to see how this can be extended to other logics, in
particular, classical logic.
The candidate should have a good background in proof theory and
Applicants should send their application (CV and recommendation
letters) to Lutz
Deadline: 30 April 2009
The position is part of the ARC Redo.
It an INRIA-postdoc position. That means that the candidate must fulfill the formal requirements for INRIA postdocs which can be found at INRIA's web-page. In particular, the candidate must have held a doctorate or Ph.D. for less than one year before the recruitment date. If the Ph.D. is not defended at the application date, you should cleary point out the defence date and the composition of jury.
The salary is 2357.30 euros gross per month.
The application process for this position is independent from the INRIA-postdoc campaign.
For further information, contact Lutz Straßburger.