A semantic characterisation of the correctness of a proof net
Christian Retoré · Mathematical Structures in Computer Science · 1997
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).