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
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