A semantic characterisation of the correctness of a proof net.

C. Retoré

Mathematical Structures in Computer Science, vol. 7(5):445--452 1997

Abstract

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 the INRIA Research Report RR-2430.

BACK