HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

From multiple sequent for Additive Linear Logic to decision procedures for Free Lattices

Jean-Yves Marion 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The additive fragment of linear logic is complete for general (non-distributive) lattices. A sequent calculus for general lattices is presented with multiple antecedents and succedents. This construction is extended to give a sequent calculus for propositional linear logic with both additive and multiplicative contexts. Then, various decision procedures are investigated for general lattices.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/inria-00098803
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 8:38:43 AM
Last modification on : Friday, February 4, 2022 - 3:33:27 AM

Identifiers

  • HAL Id : inria-00098803, version 1

Collections

Citation

Jean-Yves Marion. From multiple sequent for Additive Linear Logic to decision procedures for Free Lattices. Theoretical Computer Science, Elsevier, 1999, 224 (1-2), pp.157-172. ⟨inria-00098803⟩

Share

Metrics

Record views

47