MALL证明网识别模规则交换证明
MALL proof nets identify proofs modulo rule commutation
摘要：
我们证明了在[Hughes & van Glabbeek 2003，2005]中引入的MALL（Multiplicative Additive Linear Logic，without units）的证明网可以识别模规则交换的免割证明：两个免割证明转换为同一个证明网当且仅当一个可以通过一系列规则交换从另一个得到。这个结果在有和没有混合规则的情况下都成立，我们用cut来扩展它。
英文摘要：
We show that the proof nets introduced in [Hughes & van Glabbeek 2003, 2005] for MALL (Multiplicative Additive Linear Logic, without units) identify cut-free proofs modulo rule commutation: two cut-free proofs translate to the same proof net if and only if one can be obtained from the other by a succession of rule commutations. This result holds with and without the mix rule, and we extend it with cut.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
