Counting Proof Nets

Lutz Straßburger, INRIA Sacalay - Île-de-France

LIX, Ecole Polytechnique, Palaiseau

Proof nets are graphical structures that abstract away unnecessary bureaucracy that usually comes with formal proofs, as for example, rule permutations in sequent calculus. Thus, proof nets are concise representations of formal proofs. We can therefore reduce the question ``How many proofs does a certain formula have?'' to the question ``How many proof nets do exists for this formula?''

This way, a proof theoretical question becomes a combinatoric question. The task for this internship is apply the methods of analytic combinatorics to investigate the number of proof nets of a given size.

Basic knowledge in logic or analytic combinatorics.

Lutz Straßburger's list of problems
Parsifal's web page
Alessio Guglielmi's web page on deep inference