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

DOI10.1016/S0304-3975(98)00311-9zbMath0933.03080MaRDI QIDQ1960422

Jean-Yves Marion

Publication date: 12 January 2000

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

zbMATH Keywords

sequent calculuspropositional linear logicdecision procedurefree latticesadditive 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)

Related Items (1)

Temporal BI: proof system, semantics and translations

Uses Software

• Lolli

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Resolution calculus for the first order linear logic
• Term rewrite systems for lattice theory
• Logic programming in a fragment of intuitionistic linear logic
• Proof strategies in linear logic
• On proof normalization in linear logic
• On the word problem for the modular lattice with four free generators
• Free Modular Lattices
• Some Syntactical Observations on Linear Logic

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