Hostname: page-component-6bf8c574d5-7jkgd Total loading time: 0 Render date: 2025-02-21T23:11:28.440Z Has data issue: false hasContentIssue false

A semantic characterisation of the correctness of a proof net

Published online by Cambridge University Press:  01 October 1997

CHRISTIAN RETORÉ
Affiliation:
Projet Calligramme, INRIA-Lorraine & CRIN-C.N.R.S., 615 rue du Jardin Botanique, B.P. 101, F-54602 Villers lès Nancy Cedex, France. Email: retore@loria.fr
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

The purpose of this note is to show that the correctness of a multiplicative proof net with mix is equivalent to its semantic correctness: a proof structure is a proof net if and only if its semantic interpretation is a clique, where one given finite coherence space interprets all propositional variables.

This is just an example of what can be done with these kinds of semantic techniques; for more information and further results, the reader is referred to Retoré (1994).

Type
Research Article
Copyright
1997 Cambridge University Press