From multiple sequent for additive linear logic to decision procedures for free lattices

DOI10.1016/S0304-3975(98)00311-9MaRDI QIDQ1960422zbMATH OpenFDO

Authors Jean-Yves Marion

Publication date 12 January 2000

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

zbMATH Keywords

sequent calculusdecision procedurefree latticespropositional linear logicadditive linear logicgeneral latticesmultiple antecedents and succedents

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Free lattices, projective lattices, word problems (06B25)

Recommendations

• scientific article; zbMATH DE number 1114345
• scientific article; zbMATH DE number 1678379
• Decision problems for propositional linear logic
• scientific article; zbMATH DE number 3910455
• The finite model property for various fragments of linear logic

Cites work

• scientific article; zbMATH DE number 65760 (Why is no real title available?)
• scientific article; zbMATH DE number 1028818 (Why is no real title available?)
• scientific article; zbMATH DE number 3204690 (Why is no real title available?)
• scientific article; zbMATH DE number 3261581 (Why is no real title available?)
• Free Modular Lattices
• Linear logic
• Logic programming in a fragment of intuitionistic linear logic
• On proof normalization in linear logic
• On the word problem for the modular lattice with four free generators
• Proof strategies in linear logic
• Resolution calculus for the first order linear logic
• Some Syntactical Observations on Linear Logic
• Term rewrite systems for lattice theory

Cited in

(3)

• Temporal BI: proof system, semantics and translations
• Free algebras corresponding to multiplicative classical linear logic and some of its extensions
• Permutability of rules for linear lattices

Describes a project that uses

Uses Software

• Lolli

This page was built for publication: From multiple sequent for additive linear logic to decision procedures for free lattices

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