Admissibility of structural rules for contraction-free systems of intuitionistic logic

DOI10.2307/2695061zbMath0973.03010OpenAlexW2134005639MaRDI QIDQ2710593

Roy Dyckhoff, Sara Negri

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

zbMATH Keywords

cut eliminationintuitionistic logicsequential formulationadmissibility of contractioncontraction-free system

Mathematics Subject Classification ID

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)

Practical Proof Search for Coq by Type Inhabitation ⋮ Terminating calculi and countermodels for constructive modal logics ⋮ An intuitionistic formula hierarchy based on high‐school identities ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ Proof theory of Nelson's paraconsistent logic: a uniform perspective

Uses Software

• Unnamed Item

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