Proof net
In proof theory, proof nets are a geometrical method of representing proofs that
eliminates two forms of bureaucracy that differentiates proofs: irrelevant syntactical features of regular proof calculi such as the natural deduction calculus and the sequent calculus, and the order of rules applied in a derivation. In this way, the formal properties of proof identity correspond more closely to the intuitively desirable properties. Proof nets were introduced by Jean-Yves Girard.
For instance, these two linear logic proofs are “morally” identical:
And their corresponding nets will be the same.Several correctness criteria are known to check if a sequential proof structure is actually a concrete proof structure. The first such criterion is the long-trip criterion which was described by Jean-Yves Girard.
