Proof net
From Wikipedia, the free encyclopedia
In proof theory, proof nets are a geometrical method of representing proofs such 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. By this means the formal properties of proof identity correspond more closely to the intuitively desirable properties. Proof nets were introduced by Jean-Yves Girard.
[edit] See also
- Linear logic
- Ludics
- Geometry of interaction
- Coherent space
- Deep inference
[edit] References
- Proofs and Types. Girard J-Y, Lafont Y, and Taylor P. Cambridge Press, 1989. (An electronic version is online at [1].)