Correctness of linear logic proof structures is NL-complete

DOI10.1016/j.tcs.2010.12.020zbMath1222.03069OpenAlexW2092553770MaRDI QIDQ534703

Virgile Mogbil, Paulin Jacobé de Naurois

Publication date: 10 May 2011

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2010.12.020

zbMATH Keywords

linear logiccomplexity classesnondeterministic logspacecorrectness criteria

Mathematics Subject Classification ID

Structure of proofs (03F07) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items

Graph characterization by counting sink star subgraphs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Transcendental syntax I: deterministic case ⋮ A formal model for a linear time correctness condition of proof nets of multiplicative linear logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• The structure of multiplicatives
• The additive multiboxes
• Constant Depth Reducibility
• Undirected ST-connectivity in log-space
• Nondeterministic Space is Closed under Complementation
• New problems complete for nondeterministic log space
• Proof nets for unit-free multiplicative-additive linear logic
• Fast verification of MLL proof nets via IMLL
• Parsing MELL proof nets