This work is a first step in the study of combinatorics of proof nets: proof nets are pure geometrical objects issued from the study of linear logic, they are intended to capture the non-burocratic aspects of proofs in sequent calculus; in fact, they can be obtained from proof structures (pure combinatorial nets of rules (or links)) by adding a constraint known as ``correctness criterion'' (usually cited in the Danos-Regnier form). We try to establish the exact ratio between proof structures and proof nets, finally we can obtain only an upperbound and a lowerbound.
[ bib ]