Résumé
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).