Multiplicative-additive proof equivalence is \textsf{logspace}-complete, via binary decision trees

DOI10.23638/LMCS-13(4:20)2017zbMATH Open1433.03145arXiv1707.00991MaRDI QIDQ4596799FDOQ4596799

Authors: Marc Bagnol 

Publication date: 11 December 2017

Full work available at URL: https://arxiv.org/abs/1707.00991

Recommendations

• MALL proof equivalence is logspace-complete, via binary decision diagrams
• No proof nets for MLL with units: proof equivalence in MLL is PSPACE-complete
• Proof equivalence in MLL is PSPACE-complete
• Decision problems for propositional linear logic
• Proof nets for unit-free multiplicative-additive linear logic

zbMATH Keywords

linear logiclogarithmic spaceadditive connectivesproof equivalenceproofnets

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Structure of proofs (03F07) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Cited In (3)

• MALL proof equivalence is logspace-complete, via binary decision diagrams
• Constant-only multiplicative linear logic is NP-complete
• No proof nets for MLL with units: proof equivalence in MLL is PSPACE-complete

This page was built for publication: Multiplicative-additive proof equivalence is \textsf{logspace}-complete, via binary decision trees

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4596799)