On the relation between coherence semantics and multiplicative proof nets - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport Année : 1994

On the relation between coherence semantics and multiplicative proof nets

Résumé

It is known that (mix) proof nets admits a coherence semantics, computed as a set of experiments. We prove here the converse: a proof structure is shown to be a proof net whenever its sets of experiments is a semantical object --- a clique of the corresponding coherence space. Moreover the interpretation of atomic formulae can be restricted to a given coherent space with three tokens in its web. This is done by transforming \tt cut links into \tt tensor links. Dealing directly with non-cut-free proof structure we characterise the deadlock freeness of the reduced proof structure. These results are especially convenient for Abramsky's proof expressions, and can be extended to the pomset calculus.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
RR-2430.pdf (235.34 Ko) Télécharger le fichier
Loading...

Dates et versions

inria-00074245 , version 1 (24-05-2006)

Identifiants

  • HAL Id : inria-00074245 , version 1

Citer

Christian Retoré. On the relation between coherence semantics and multiplicative proof nets. RR-2430, INRIA. 1994. ⟨inria-00074245⟩
139 Consultations
182 Téléchargements

Partager

Gmail Facebook X LinkedIn More