Editing 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.  This distinguishes proof nets from regular proof calculi such as the [[natural deduction]] calculus and the [[sequent calculus]], where these phenomena are present. Proof nets were introduced by [[Jean-Yves Girard]]. 

As an illustration, these two [[linear logic]] proofs are identical:

{| style="margin:0.5em auto"
|-
| style="text-align: center; padding-right: 40px" |
{| border="0"
|-
| {{math|{{tee}} <VAR>A</VAR>, <VAR>B</VAR>, <VAR>C</VAR>, <VAR>D</VAR>}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} <VAR>A</VAR> ⅋ <VAR>B</VAR>, <VAR>C</VAR>, <VAR>D</VAR>}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} <VAR>A</VAR> ⅋ <VAR>B</VAR>, <VAR>C</VAR> ⅋ <VAR>D</VAR>}}
|}
| style="text-align: center;" |
{| border="0"
|-
| {{math|{{tee}} <VAR>A</VAR>, <VAR>B</VAR>, <VAR>C</VAR>, <VAR>D</VAR>}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} <VAR>A</VAR>, <VAR>B</VAR>, <VAR>C</VAR> ⅋ <VAR>D</VAR>}}
|-
| style="border-top:2px solid black;" |
|-
| {{math|{{tee}} <VAR>A</VAR> ⅋ <VAR>B</VAR>, <VAR>C</VAR> ⅋ <VAR>D</VAR>}}
|}
|}

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 that seems to be a proof net) is actually a concrete proof structure (i.e. something that encodes a valid derivation in linear logic). The first such criterion is the [[long-trip criterion]],<ref>Girard, Jean-Yves. ''[http://girard.perso.math.cnrs.fr/linear.pdf Linear logic]'', [[Theoretical Computer Science (journal)|Theoretical Computer Science]], Vol 50, no 1, pp.&nbsp;1–102, 1987</ref> which was described by [[Jean-Yves Girard]].

==See also==
* [[Linear logic]]
* [[Ludics]]
* [[Geometry of interaction]]
* [[Coherent space]]
* [[Deep inference]]
* [[Interaction nets]]

==References==
<references />

==Sources ==
* ''[http://www.paultaylor.eu/stable/Proofs+Types.html Proofs and Types]''.  Girard J-Y, Lafont Y, and Taylor P.  Cambridge Press, 1989.
* [[Roberto Di Cosmo]] and Vincent Danos, [http://www.dicosmo.org/CourseNotes/LinLog/ The Linear Logic Primer]
* Sean A. Fulop, [https://arxiv.org/abs/1203.4912 A survey of proof nets and matrices for substructural logics]

[[Category:Proof theory]]

{{logic-stub}}