MALL的抽象p-时间证明网：冲突网
Abstract p-time proof nets for MALL: Conflict nets
摘要：
本文提出了乘加线性逻辑（MALL）的证明网，称为冲突网。它们是有效的，因为证明的正确性和翻译都是p-时间（多项式时间），并且是抽象的，因为它们在转置相邻的&-规则下是不变的。一个抽象上的冲突网是简洁的：公理与冲突关系相联系。冲突网是最近为经典逻辑引入的组合证明的一个变体（并受到其启发）：每一个都可以被视为可收缩相干空间（P_4-free graphs，或cographs）的极大映射（同态），从公理到公理。本文给出了其他证明网的新结果：（1）切片网（Hughes/van Glabbeek 2003）的正确性和割消是p-时间的;（2）单项式网（Girard 1996）的割消不起作用。打破单项网割消的微妙之处也适用于冲突网：与单项网一样，合流割消的存在仍然是一个悬而未决的问题。
英文摘要：
This paper presents proof nets for multiplicative-additive linear logic (MALL), called conflict nets. They are efficient, since both correctness and translation from a proof are p-time (polynomial time), and abstract, since they are invariant under transposing adjacent &-rules. A conflict net on a sequent is concise: axiom links with a conflict relation. Conflict nets are a variant of (and were inspired by) combinatorial proofs introduced recently for classical logic: each can be viewed as a maximal map (homomorphism) of contractible coherence spaces (P_4-free graphs, or cographs), from axioms to sequent. The paper presents new results for other proof nets: (1) correctness and cut elimination for slice nets (Hughes / van Glabbeek 2003) are p-time, and (2) the cut elimination proposed for monomial nets (Girard 1996) does not work. The subtleties which break monomial net cut elimination also apply to conflict nets: as with monomial nets, existence of a confluent cut elimination remains an open question.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
