Abstract p-time proof nets for MALL: Conflict nets

TL;DR

This paper introduces conflict nets for MALL, a new class of proof nets that are efficient, invariant under certain rule transpositions, and inspired by combinatorial proofs, with new results on correctness and cut elimination.

Contribution

It presents conflict nets for MALL that are polynomial-time correct and transposition-invariant, and compares them with other proof net variants, highlighting their advantages and open problems.

Findings

Correctness and cut elimination for slice nets are p-time.

Cut elimination for monomial nets does not work.

Existence of confluent cut elimination for conflict nets remains open.

Abstract

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.