Proof net

In proof theory, proof nets are a geometrical method of representing proofs that eliminates two forms of bureaucracy that differentiate proofs: (A) irrelevant syntactical features of regular proof calculi, 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. This distinguishes proof nets from regular proof calculi such as the natural deduction calculus and the sequent calculus, where these phenomena are present.

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.