Correctness of linear logic proof structures is NL-complete

DOI10.1016/J.TCS.2010.12.020zbMATH Open1222.03069OpenAlexW2092553770MaRDI QIDQ534703FDOQ534703

Authors: Paulin Jacobé de Naurois, Virgile Mogbil 

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

Recommendations

• Correctness of Multiplicative (and Exponential) Proof Structures is NL-Complete
• On \(\text{NP}\)-completeness in linear logic
• Proofs as computations in linear logic
• scientific article; zbMATH DE number 1292302
• Correctness and completeness of logic programs
• scientific article; zbMATH DE number 786489
• Completeness for linear continuous logic
• Compact proof certificates for linear logic
• The semantics and proof theory of linear logic
• Proof method of partial correctness and weak completeness for normal logic programs

zbMATH Keywords

complexity classeslinear logicnondeterministic logspacecorrectness criteria

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (7)

• Graph characterization by counting sink star subgraphs
• Title not available (Why is that?)
• Transcendental syntax I: deterministic case
• PSPACE-completeness of a thread criterion for circular proofs in linear logic with least and greatest fixed points
• Title not available (Why is that?)
• Correctness of Multiplicative (and Exponential) Proof Structures is NL-Complete
• A formal model for a linear time correctness condition of proof nets of multiplicative linear logic

This page was built for publication: Correctness of linear logic proof structures is NL-complete

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