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:
And their corresponding nets will be the same.
Correctness criteria
Several correctness criteria are known to check if a sequential proof structure (i.e. something which seems to be a proof net) is actually a concrete proof structure (i.e. something which encodes a valid derivation in linear logic). The first such criterion is the
long-trip criterion[Girard, Jean-Yves. ]
Linear logic
', Theoretical Computer Science, Vol 50, no 1, pp. 1–102, 1987 which was described by
Jean-Yves Girard.
See also
*
Linear logic
*
Ludics
*
Geometry of interaction
*
Coherent space
*
Deep inference
Deep inference names a general idea in structural proof theory that breaks with the classical sequent calculus by generalising the notion of structure to permit inference to occur in contexts of high structural complexity. The term ''deep infer ...
*
Interaction nets
References
Sources
*
Proofs and Types'. Girard J-Y, Lafont Y, and Taylor P. Cambridge Press, 1989.
* Roberto Di Cosmo and Vincent Danos
The Linear Logic Primer* Sean A. Fulop
A survey of proof nets and matrices for substructural logics
Proof theory
{{logic-stub