Handsome Proof-nets: R&B-Graphs, Perfect Matchings and Series-parallel Graphs
Résumé
The main interest of this paper is to provide proof-nets, a proof syntax which identify proofs with the same meaning, with a standard graph-theoretical description. More precisely, we give two such descriptions which both view proof-nets as graphs endowed with a perfect matching, and in both cases the graphs corresponding to proofs are recognized by a simple correctnes- s criterion (with and without the so-called mix rule). The first description may be viewed as a graph-theoretical reformulation of usual proof-nets; nevertheless it allows us to recover various results on proof-nets as the corollaries of a single graph theoretical result. The second description, inspired from the first one, is more innovative: a proof-structure simply consists in the set of its axioms - the perfect matching - plus one single series-parallel graph (a.k.a cograph) which encodes the whole syntactical forest of the sequent. Unlike other approaches, every such graph, with out any further specification, corresponds to a proof structure, and this description identify proof structures which only differ up to the commutativity or associativity of the connectives, or because final disjunctions have been performed or not. Thus these proof-nets are even closer to the proofs themselves than usual proof-nets.
Domaines
Autre [cs.OH]
Loading...