Linearizing intuitionistic implication

DOI10.1016/0168-0072(93)90041-BzbMath0767.03006MaRDI QIDQ1210141

Natarajan Shankar, Andrej Scedrov, Patrick D. Lincoln

Publication date: 16 May 1993

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

linear logiccut-free proofintuitionistic logic

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

First-order linear logic without modalities is NEXPTIME-hard, Towards NP-P via proof complexity and search, Intuitionistic Decision Procedures Since Gentzen, Proof-search in intuitionistic logic based on constraint satisfaction, Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi

Uses Software

• Lolli

Cites Work

• Linear logic
• Computational interpretations of linear logic
• The linear abstract machine
• A game semantics for linear logic
• Decision problems for propositional linear logic
• Bounded linear logic: A modular approach to polynomial-time computability
• Intuitionistic propositional logic is polynomial-space complete
• Accessible categories and models of linear logic
• Uniform proofs as a foundation for logic programming
• Logic Programming with Focusing Proofs in Linear Logic
• Contraction-free sequent calculi for intuitionistic logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item