Gentzen's Proof of Normalization for Natural Deduction
From MaRDI portal
Recommendations
- Gentzen's proof systems: byproducts in a work of genius
- scientific article; zbMATH DE number 4035774
- Saved from the cellar. Gerhard Gentzen's shorthand notes on logic and foundations of mathematics
- A sequent calculus isomorphic to Gentzen's natural deduction
- A note on how to extend Gentzen's second consistency proof to a proof of normalization for first order arithmetic
Cites work
Cited in
(32)- Normal natural deduction proofs (in classical logic)
- Stabilizing quantum disjunction
- Bilateralism does not provide a proof theoretic treatment of classical logic (for technical reasons)
- Human-centered automated proof search
- Maximum segments as natural deduction images of some cuts
- Normalisation and subformula property for a system of classical logic with Tarski's rule
- Translations between Gentzen-Prawitz and Jaśkowski-Fitch natural deduction proofs
- Normality, non-contamination and logical depth in classical natural deduction
- On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
- Proof-theoretic harmony: towards an intensional account
- Generality and existence: quantificational logic in historical perspective
- On natural deduction for Herbrand constructive logics. I: Curry-Howard correspondence for Dummett's logic \(\mathsf {LC}\)
- A sequent calculus isomorphic to Gentzen's natural deduction
- Cut as consequence
- AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ
- scientific article; zbMATH DE number 1406467 (Why is no real title available?)
- The problem of apagogic proof in Bolzano's \textit{Contributions} and his \textit{Theory of science}
- Proofs as Objects
- Prawitz, Proofs, and Meaning
- Inversion principles and introduction rules
- Meaning in use
- Saved from the cellar. Gerhard Gentzen's shorthand notes on logic and foundations of mathematics
- A note on how to extend Gentzen's second consistency proof to a proof of normalization for first order arithmetic
- Dialogues and Proofs; Yankov’s Contribution to Proof Theory
- General-elimination harmony and the meaning of the logical constants
- An ecumenical notion of entailment
- Adding Negation to Lambda Mu
- The elimination of maximum cuts in linear logic and BCK logic
- Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules
- Harmony in the light of computational ludics
- Sequent images of normal derivations and natural deduction images of derivations without m-cuts
- Mind the gap: a conciliating short proof of strong normalization for minimal propositional logic
This page was built for publication: Gentzen's Proof of Normalization for Natural Deduction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3503742)
