Editing Linear logic (section)

===Proof nets===
{{main|Proof net}}

Introduced by [[Jean-Yves Girard]], proof nets have been created to avoid the ''bureaucracy'', that is all the things that make two derivations different in the logical point of view, but not in a "moral" point of view.

For instance, these two proofs are "morally" identical:
{| style="margin:auto"
|-
| 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>}}
|}
| 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>}}
|}
|}

The goal of proof nets is to make them identical by creating a graphical representation of them.