A linear algorithm for MLL proof net correctness and sequentialization

DOI10.1016/J.TCS.2010.12.021MaRDI QIDQ534705zbMATH OpenOpenAlexFDO

Authors Stefano Guerrini

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.021

zbMATH Keywords

proof netsmultiplicative linear logic

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Structure of proofs (03F07) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• Fast verification of MLL proof nets via IMLL
• A new correctness criterion for the proof nets of non-commutative multiplicative linear logics
• Sequent reconstruction in LLM -- A sweepline proof
• scientific article; zbMATH DE number 1222110
• Correctness of Multiplicative (and Exponential) Proof Structures is NL-Complete

Cites work

• scientific article; zbMATH DE number 786495 (Why is no real title available?)
• A linear-time algorithm for a special case of disjoint set union
• A new correctness criterion for the proof nets of non-commutative multiplicative linear logics
• An Efficient Unification Algorithm
• Correctness of Multiplicative (and Exponential) Proof Structures is NL-Complete
• Efficiency of a Good But Not Linear Set Union Algorithm
• Fast verification of MLL proof nets via IMLL
• Linear logic
• Parsing MELL proof nets
• The structure of multiplicatives

Cited in

(12)

• Study of behaviours via visitable paths
• A coding theoretic study of MLL proof nets
• Fast verification of MLL proof nets via IMLL
• Sequent reconstruction in LLM -- A sweepline proof
• Linear time proof verification on N-graphs: a graph theoretic approach
• Learning Lambek grammars from proof frames
• Unification nets: canonical proof net quantifiers
• scientific article; zbMATH DE number 7359421 (Why is no real title available?)
• Proof nets for multiplicative cyclic linear logic and Lambek calculus
• The sum-product algorithm for quantitative multiplicative linear logic
• 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: A linear algorithm for MLL proof net correctness and sequentialization

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