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