“Proof net”的意思、由来-开放百科全书

词条

Proof net

释义

Correctness criteria
See also
References
Sources

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:

{{tee}} A, B, C, D}}

{{tee}} A ⅋ B, C, D}}

{{tee}} A ⅋ B, C ⅋ D}}

{{tee}} A, B, C, D}}

{{tee}} A, B, C ⅋ D}}

{{tee}} A ⅋ B, C ⅋ D}}

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^[1] which was described by Jean-Yves Girard.

References

1. ^Girard, Jean-Yves. Linear logic, Theoretical Computer Science, Vol 50, no 1, pp. 1–102, 1987

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, [https://arxiv.org/abs/1203.4912 A survey of proof nets and matrices for substructural logics]

1 : Proof theory

随便看

开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。

Correctness criteria

See also

References

Sources