Handsome Proof-nets: R&B-Graphs, Perfect Matchings and Series-parallel Graphs

Christian Retoré 1
1 PARAGRAPHE - Parallelism and Graphs
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
Abstract : 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.
Type de document :
[Research Report] RR-3652, INRIA. 1999
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 11:37:03
Dernière modification le : vendredi 16 novembre 2018 - 01:23:53
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:31:31



  • HAL Id : inria-00073020, version 1


Christian Retoré. Handsome Proof-nets: R&B-Graphs, Perfect Matchings and Series-parallel Graphs. [Research Report] RR-3652, INRIA. 1999. 〈inria-00073020〉



Consultations de la notice


Téléchargements de fichiers