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
Jean-Yves Girard (; born 1947) is a French logician working in proof theory. He is the research director (emeritus) at the mathematical institute of the University of Aix-Marseille, at Luminy.
Biography
Jean-Yves Girard is an alumnus of the ...
. This distinguishes proof nets from regular proof calculi such as the
natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use ax ...
calculus and the
sequent calculus
In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology i ...
, 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
Jean-Yves Girard (; born 1947) is a French logician working in proof theory. He is the research director (emeritus) at the mathematical institute of the University of Aix-Marseille, at Luminy.
Biography
Jean-Yves Girard is an alumnus of the ...
.
See also
*
Linear logic
*
Ludics
In proof theory, ludics is an analysis of the principles governing inference rules of mathematical logic. Key features of ludics include notion of compound connectives, using a technique known as ''focusing'' or ''focalisation'' (invented by the ...
*
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 inferenc ...
*
Interaction nets Interaction nets are a graphical model of computation devised by Yves Lafont in 1990 as a generalisation of the proof structures of linear logic. An interaction net system is specified by a set of agent types and a set of interaction rules. Intera ...
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