Pomset Logic as a Calculus of Directed Cographs

Christian Retoré 1
1 PARAGRAPHE - Parallelism and Graphs
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
Abstract : We give an abstract formulation of proof-structures and nets for pomset logic i.e. linear logic enriched with a non commutative and self-dual connective. A proof-structure is described as a directed R&B-cograph, that is an edge bicoloured graph: one colour is a perfect matching and the other a directed cograph - directed cographs are a simple generalization of cographs and series-parallel orders. The proof-nets or correct proof-struct- ures are the directed R&B-cographs such that every alternate elementary circuit contains a chord. This representation is even more compact than usual descriptions: the algebraic properties of the connectives, associativity and commutativity, are interpreted by equality, as well as the presence or not of final disjunctions (final par's). But the main advantage is that any directed R&B-cograph, without any further specification, is a proof-structure. We then study a step by step invertible transformation from proof-structures with links to directed R&B-cographs; this transformation and its inverse preserve correctness. Next we study the impact of the graph rewriting which axiomatizes the inclusion of directed cographs (found with D. Bechet and Ph. de Groote) on the correctness of directed R&B-cographs, and we show that all rewriting rules but one preserve the correctness. This yields cut-elimination (strongly normalizing and confluent) and suggests a complete sequent calculus for Pomset logic. These results also apply to linear logic enriched with the mix rule, since Pomset logic is a conservati- ve extension of it.
Type de document :
[Research Report] RR-3714, INRIA. 1999
Liste complète des métadonnées

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

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



  • HAL Id : inria-00072953, version 1


Christian Retoré. Pomset Logic as a Calculus of Directed Cographs. [Research Report] RR-3714, INRIA. 1999. 〈inria-00072953〉



Consultations de la notice


Téléchargements de fichiers