inria-00074245, version 1

On the relation between coherence semantics and multiplicative proof nets

Christian Retoré (, ) ¹

N° RR-2430 (1994)

• 1:  MEIJE (INRIA Sophia Antipolis)
• 
  INRIA France

Bibliographic reference

• Type of document: Research reports
• Domain: Computer Science/Other
• Title: On the relation between coherence semantics and multiplicative proof nets
• Abstract: 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.
• Full text language: English
• Publication date: 1994-12
• Keywords: LOGIC / PROOF THEORY / LINEAR LOGIC / PROOF NETS / DENOTATIONAL SEMANTICS
• Writing date: 1994-12
• Internal note: RR-2430

Attached file list to this document: 

• inria-00074245, version 1
• http://hal.inria.fr/inria-00074245
• oai:hal.inria.fr:inria-00074245
• From: Rapport De Recherche Inria <>
• Submitted on: Wednesday, 24 May 2006 14:51:02
• Updated on: Wednesday, 31 May 2006 14:24:32