Correctness of linear logic proof structures is NL-complete

DOI10.1016/J.TCS.2010.12.020MaRDI QIDQ534703zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 4087055 (Why is no real title available?)
• scientific article; zbMATH DE number 2134917 (Why is no real title available?)
• scientific article; zbMATH DE number 786495 (Why is no real title available?)
• scientific article; zbMATH DE number 937366 (Why is no real title available?)
• Constant Depth Reducibility
• Fast verification of MLL proof nets via IMLL
• Linear logic
• New problems complete for nondeterministic log space
• Nondeterministic Space is Closed under Complementation
• Parsing MELL proof nets
• Proof nets for unit-free multiplicative-additive linear logic
• The additive multiboxes
• The structure of multiplicatives
• Undirected ST-connectivity in log-space

Cited in

(7)

• Graph characterization by counting sink star subgraphs
• scientific article; zbMATH DE number 7359421 (Why is no real title available?)
• PSPACE-completeness of a thread criterion for circular proofs in linear logic with least and greatest fixed points
• Transcendental syntax I: deterministic case
• scientific article; zbMATH DE number 7359406 (Why is no real title available?)
• 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)