Proof net

In proof theory, proof nets are a geometrical method of representing proofs that eliminates two forms of bureaucracy that differentiates proofs: (A) irrelevant syntactical features of regular proof calculi such as the natural deduction calculus and the sequent calculus, and (B) 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 identical:

${\displaystyle \vdash }$ A, B, C, D ${\displaystyle \vdash }$ A ⅋ B, C, D ${\displaystyle \vdash }$ A ⅋ B, C ⅋ D

${\displaystyle \vdash }$ A, B, C, D ${\displaystyle \vdash }$ A, B, C ⅋ D ${\displaystyle \vdash }$ A ⅋ B, C ⅋ D

And their corresponding nets will be the same.