Correctness of Multiplicative (and Exponential) Proof Structures is NL -Complete

We provide a new correctness criterion for unit-free MLL proof structures and MELL proof structures with units. We prove that deciding the correctness of a MLL and of a MELL proof structure is NL-complete. We also prove that deciding the correctness of an intuitionistic multiplicative essential net is NL-complete.

• Type: Conference
• Year: 2007
• Where: CSL
• Authors: Paulin Jacobé de Naurois, Virgile Mogbil
• Keywords: Correctness, CSL 2007, Mell Proof Structure, MLL Proof Structures