Admissibility of structural rules for contraction-free systems of intuitionistic logic
DOI10.2307/2695061zbMath0973.03010OpenAlexW2134005639MaRDI QIDQ2710593
Publication date: 16 July 2001
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2695061
cut eliminationintuitionistic logicsequential formulationadmissibility of contractioncontraction-free system
Cut-elimination and normal-form theorems (03F05) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items (5)
Uses Software
Cites Work
- Unnamed Item
- Bounds for cut elimination in intuitionistic propositional logic
- Isabelle. A generic theorem prover
- Sequent calculus proof theory of intuitionistic apartness and order relations
- On an interpretation of second order quantification in first order intuitionistic propositional logic
- An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
- Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic
- A new algorithm for derivability in the constructive propositional calculus
This page was built for publication: Admissibility of structural rules for contraction-free systems of intuitionistic logic