Linearizing intuitionistic implication

DOI10.1016/0168-0072(93)90041-BMaRDI QIDQ1210141zbMATH OpenFDO

Authors Natarajan Shankar, P. Lincoln, Andre Scedrov

Publication date 16 May 1993

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

Full work available at URL https://doi.org/10.1016/0168-0072(93)90041-B

zbMATH Keywords

cut-free proofintuitionistic logiclinear logic

Mathematics Subject Classification ID

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

Recommendations

• Reductions in Intuitionistic Linear Logic
• Natural deduction for intuitionistic linear logic
• Reflections on ``difficult embeddings
• Functional Interpretations of Intuitionistic Linear Logic
• Around classical and intuitionistic linear logics

Cites work

• A game semantics for linear logic
• Accessible categories and models of linear logic
• Bounded linear logic: A modular approach to polynomial-time computability
• Computational interpretations of linear logic
• Contraction-free sequent calculi for intuitionistic logic
• Decision problems for propositional linear logic
• scientific article; zbMATH DE number 3142912 (Why is no real title available?)
• scientific article; zbMATH DE number 4209572 (Why is no real title available?)
• scientific article; zbMATH DE number 4055576 (Why is no real title available?)
• scientific article; zbMATH DE number 15881 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 47007 (Why is no real title available?)
• scientific article; zbMATH DE number 4123722 (Why is no real title available?)
• scientific article; zbMATH DE number 3231072 (Why is no real title available?)
• scientific article; zbMATH DE number 3261581 (Why is no real title available?)
• scientific article; zbMATH DE number 3031479 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• Intuitionistic propositional logic is polynomial-space complete
• Linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• The linear abstract machine
• Uniform proofs as a foundation for logic programming

Cited in

(10)

• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• First-order linear logic without modalities is NEXPTIME-hard
• Classical multiplicative linear logic intuitionistic MLL
• Intuitionistic Decision Procedures Since Gentzen
• Modeling linear logic with implicit functions
• Towards NP-P via proof complexity and search
• Proof-search in intuitionistic logic based on constraint satisfaction
• Reductions in Intuitionistic Linear Logic
• Intuitionistic phase semantics is almost classical
• Worst-case input generation for concurrent programs under non-monotone resource metrics

Describes a project that uses

Uses Software

• Lolli

This page was built for publication: Linearizing intuitionistic implication

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1210141)