Expansion Nets: Proof-Nets for Propositional Classical Logic

We give a calculus of proof-nets for classical propositional logic. These nets improve on a proposal due to Robinson by validating the associativity and commutativity of contraction, and provide canonical representants for classical sequent proofs modulo natural equivalences. We present the relationship between sequent proofs and proof-nets as an annotated sequent calculus, deriving formulae decorated with expansion/deletion trees. We then show a subcalculus, expansion nets, which in addition to these good properties has a polynomial-time correctness criterion.