Title: Case study: Additive linear logic and lattices
Abstract: We investigate sequent calculus where contexts, called additive contexts, are governed by the operations of a non-distributive lattice. We present a sequent calculus ALL m with multiple antecedents and succedents. ALL m is complete for non-distributive lattices and is equivalent to the additive fragment of linear logic. Weakenings and contractions are postulated for ALL m and cut is redundant. We extend this construction in order to get a sequent calculus for propositional linear logic with both additive and multiplicative contexts. Then we show that a bottom-up decision procedure based on the cut-free sequent calculi runs in exponential time. We provide a decision algorithm that exploits analytic cuts and whose runtime is polynomial.
Publication Year: 1997
Publication Date: 1997-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 1
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot