Handsome proof-nets: perfect matchings and cographs

摘要

We first extract the combinatorial result behind various proofs of the sequentialisation theorem for multiplicative proof-nets. This result is an inductive characterisation of graphs with a unique perfect matching. Extending these techniques, we give a definition of multiplicative proof-nets in which commutativity but also associativity of the multiplicative connectives is interpreted as equality. This is done by representing a sequent by a cograph and axioms by a perfect matching. The main advantage of this presentation is aesthetic: any such graph, without any further requirement is a proof-structure and the correctness criterion also is a natural graph-theoretical property. A direct and purely graph theoretical proof of these results is available as a research report in which more details can be found (C. Retore, Handsome proof-nets: R&B-graphs, perfect matchings and series-parallel graphs, Rapport de Recherche RR-3652, INRIA, March 1999.