Perfect matchings and series-parallel graphs: multiplicatives proof nets as R&B-graphs
Christian Retoré · Electronic Notes in Theoretical Computer Science · 1996
A graph-theoretical look at multiplicative proof nets lead us to two new descriptions of a proof net, both as a graph endowed with a perfect matching. The first one is a rather conventional encoding of the connectives which nevertheless allows us to unify various sequentialisation techniques as the corollaries of a single graph theoretical result. The second one is more exciting: a proof net simply consists in the set of its axioms — the perfect matching — plus one single series-parallel graph which encodes the whole syntactical forest of the sequent. We thus identify proof nets which only differ because of the commutativity or associativity of the connectives, or because final par have been performed or not. We thus push further the program of proof net theory which is to get closer to the proof itself, ignoring as much as possible the syntactical “bureaucracy”.