A SEQUENT CALCULUS ISOMORPHIC TO GENTZEN’S NATURAL DEDUCTION
From MaRDI portal
Publication:3005996
DOI10.1017/S1755020310000195zbMath1239.03034MaRDI QIDQ3005996
Publication date: 10 June 2011
Published in: The Review of Symbolic Logic (Search for Journal in Brave)
03F05: Cut-elimination and normal-form theorems
03F10: Functionals in proof theory
03F03: Proof theory in general (including proof-theoretic semantics)
Related Items
AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ, The elimination of maximum cuts in linear logic and BCK logic, Maximum segments as natural deduction images of some cuts, NORMAL DERIVABILITY IN CLASSICAL NATURAL DEDUCTION, Gentzen's Proof Systems: Byproducts in a Work of Genius
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Natural deduction with general elimination rules
- Untersuchungen über das logische Schliessen. I
- Gentzen's Proof of Normalization for Natural Deduction
- The correspondence between cut-elimination and normalization
- Normalization as a homomorphic image of cut-elimination
- Translations from natural deduction to sequent calculus
- A proof of Gentzen's \textit{Hauptsatz} without multicut