On the Computational Complexity of Cut-Elimination in Linear Logic

Abstract. Given two proofs in a logical system with a confluent cutelimination procedure, the cut-elimination problem (CEP) is to decide whether these proofs reduce to the same normal form. This decision problem has been shown to be ptime-complete for Multiplicative Linear Logic (Mairson 2003). The latter result depends upon a restricted simulation of weakening and contraction for boolean values in MLL; in this paper, we analyze how and when this technique can be generalized to other MLL formulas, and then consider CEP for other subsystems of Linear Logic. We also show that while additives play the role of nondeterminism in cut-elimination, they are not needed to express deterministic ptime computation. As a consequence, affine features are irrelevant to expressing ptime computation. In particular, Multiplicative Light Linear Logic (MLLL) and Multiplicative Soft Linear Logic (MSLL) capture ptime even without additives nor unrestricted weakening. We establish hierarchical results on th...

• Type: Conference
• Year: 2003
• Where: ICTCS
• Authors: Harry G. Mairson, Kazushige Terui
• Keywords: Cut-elimination Problem, ICTCS 2003, Linear Logic, Multiplicative Linear Logic