Linearizing intuitionistic implication
In the introduction the authors give a nice description of how linear logic is obtained from classical and intuitionistic logic by a modification in three steps. IIL denotes Implicational propositional Intuitionistic Logic. And IMALL is the Intuitionistic fragment of Multiplicative-Additive Linear Logic. Contrary to IIL, IMALL has neither contraction nor weakening and expressly forbids the copying of the principal formula of any rule into a premise. IIL* results from IIL by modifying one of its rules and by discarding the cut and contraction rules. The advantage of IIL* is that there is no copying of principal formulas. Lemmas 3.2 and 3.4 state that given a proof of \(\Gamma\vdash C\) in IIL, a proof of \(\Gamma\vdash C\) can be constructed in ILL*, and, conversely, given a proof of \(\Gamma\vdash C\) in IIL*, a proof of \(\Gamma\vdash C\) can be constructed in IIL. The lack of contraction in IIL* makes the formulation of the sequent rules for implicational intuitionistic propositional logic amenable to encoding into IMALL. For any IIL* sequent \(\Gamma\vdash C\) let \(\theta(\Gamma\vdash C)\) be its translation into IMALL. The authors show in section 5 that there exists a cut-free proof of \(\Gamma\vdash C\) in IIL* if and only if there is a cut- free proof of \(\theta(\Gamma\vdash C)\) in IMALL. This establishes their Theorem 1.1: IIL can be embedded into IMALL. The embedding preserves the structure of cut-free proofs in IIL*. In section 6 the authors show that the embedding is efficient and provides an alternative proof of the PSPACE-hardness of IMALL.
- 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
- 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
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)
