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

• Cook, S.A., McKenzie, P.: Problems complete for deterministic logarithmic space. J. Algorithms 8(3), 385–394 (1987)

  Article  MATH  MathSciNet  Google Scholar 

• Chandra, A.K., Stockmeyer, L.J., Vishkin, U.: Constant depth reducibility. SIAM J. Comput. 13(2), 423–439 (1984)

  Article  MATH  MathSciNet  Google Scholar 

• Danos, V.: Une application de la logique linéaire à l’étude des processus de normalisation (principalement de λ-calcul). PhD thesis, Université Denis Diderot, Paris 7 (1990)

  Google Scholar 

• Danos, V., Regnier, L.: The structure of multiplicatives. Archive for Mathematical Logic 28(3), 181–203 (1989)

  Article  MATH  MathSciNet  Google Scholar 

• Girard, J.-Y.: Linear logic. Theoretical Computer Science 50(1), 1–102 (1987)

  Article  MATH  MathSciNet  Google Scholar 

• Guerrini, S., Masini, A.: Parsing MELL proof nets. Theoretical Computer Science 254(1–2), 317–335 (2001)

  Article  MATH  MathSciNet  Google Scholar 

• Guerrini, S.: Correctness of multiplicative proof nets is linear. In: Proc. of the annual Symp. on Logic in Computer Science (LICS 1999), pp. 454–463. IEEE Computer Society Press, Los Alamitos (1999)

  Google Scholar 

• Immerman, N.: Nondeterministic space is closed under complementation. SIAM J. Comput. 17(5), 935–938 (1988)

  Article  MATH  MathSciNet  Google Scholar 

• Jones, N.D., Lien, Y.E., Laaser, W.T.: New problems complete for nondeterministic logspace. Mathematical Syst. Theory 10, 1–17 (1976)

  Article  MATH  MathSciNet  Google Scholar 

• Jenner, B., Lange, K.-J., McKenzie, P.: Tree isomorphism and some other complete problems for deterministic logspace. DIRO 1059, Univ. de Montréal (1997)

  Google Scholar 

• Kanovich, M.I.: Horn programming in linear logic is NP-complete. In: Proc. of the annual Symp. on Logic in Computer Science (LICS 1992), pp. 200–210. IEEE Computer Society Press, Los Alamitos (1992)

  Google Scholar 

• Lafont, Y.: From proof-nets to interaction nets. In: Girard, J.-Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic, vol. 222, pp. 225–247. Cambridge University Press, Cambridge (1995)

  Google Scholar 

• Mairson, H.G.: Normalization bounds for multiplicative linear logic are axiom-sensitive. In: GEOCAL 2006 Workshop of Implicit Computational Complexity. Slides available at http://www-lipn.univ-paris13.fr/~baillot/GEOCAL06/SLIDES/Mairson.pdf

• Melliès, P.-A.: A topological correctness criterion for non-commutative logic. London Mathematical Society Lecture Notes Series, vol. 316. Cambridge University Press, Cambridge (2004)

  Google Scholar 

• Murawski, A., Ong, L.: Dominator trees and fast verification of proof nets. In: Proc. of the annual Symp. on Logic in Computer Science (LICS 2000), pp. 181–191. IEEE Computer Society Press, Los Alamitos (2000)

  Google Scholar 

• Murawski, A., Ong, L.: Fast verification of MLL proof nets via IMLL. ACM Trans. Comput. Logic 7(3), 473–498 (2006)

  Article  MathSciNet  Google Scholar 

• Reingold, O.: Undirected st-connectivity in log-space. In: Gabow, H.N., Fagin, R. (eds.) STOC, pp. 376–385. ACM, New York (2005)

  Google Scholar 

• Szelepcsényi, R.: The method of forcing for nondeterministic automata. Bulletin of the EATCS 33, 96–99 (1987)

  MATH  Google Scholar 

Download references