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

DOI10.1016/S0304-3975(98)00311-9zbMATH Open0933.03080MaRDI QIDQ1960422FDOQ1960422

Authors: Jean-Yves Marion 

Publication date: 12 January 2000

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Linear logic
• Logic programming in a fragment of intuitionistic linear logic
• Free Modular Lattices
• Title not available (Why is that?)
• Some Syntactical Observations on Linear Logic
• On proof normalization in linear logic
• Term rewrite systems for lattice theory
• 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

Cited In (3)

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

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)