Proof net  From Wikipedia, the free encyclopedia Jump to:
navigation, search  In proof theory, proof nets are a
geometrical method of representing proofs 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. 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.  For instance, these two linear logic proofs
are “morally” identical:  \vdash A, B, C, D \vdash A B, C, D
\vdash A B, C D \vdash A, B, C, D \vdash A, B, C D \vdash A B, C
D  And their corresponding nets will be the same.  Correctness
criteria[edit]  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 der