Optimization complexity of linear logic proof games

A class of linear logic proof games is developed, each with a numeric score that depends on the number of preferred axioms used in a complete or parti al proof tree. The complexity of these games is analyzed for the NP-complet e multiplicative fragment (MLL) extended with additive constants and the PS PACE-complete multiplicative, additive fragment (MALL) of propositional lin ear logic. In each case, it is shown that it is as hard to compute an appro ximation of the best possible score as it is to determine the optimal strat egy. Furthermore, it is shown that no efficient heuristics exist unless the re is an unexpected collapse in the complexity hierarchy. (C) 1999 Publishe d by Elsevier Science B.V. All rights reserved.