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 “morally” identical:
|
|
And their corresponding nets will be the same.
Read more about Proof Net: Correctness Criteria
Famous quotes containing the words proof and/or net:
“The fact that several men were able to become infatuated with that latrine is truly the proof of the decline of the men of this century.”
—Charles Baudelaire (1821–1867)
“it was you untying the snarls and knots,
the webs, all bloody and gluey;
you with your twelve tongues and twelve wings
beating, wresting, beating, beating
your way out of childhood,
that airless net that fastened you down.”
—Anne Sexton (1928–1974)