Proof Terms for Generalized Natural Deduction

DOI10.4230/lipics.types.2017.3zbMath1528.03226OpenAlexW2909043315MaRDI QIDQ6060674

Herman Geuvers, Tonny Hurkens

Publication date: 3 November 2023

Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2018/10051/

zbMATH Keywords

natural deductionconstructive logicdetour conversionpermutation conversionnormalization curry-Howard isomorphism

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A note on harmony
• Lectures on the Curry-Howard isomorphism
• Natural deduction with general elimination rules
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Harmony and autonomy in classical logic
• The duality of computation
• Ultimate Normal Forms for Parallelized Natural Deductions
• A natural extension of natural deduction
• Inversion Principles and Introduction Rules
• Deriving Natural Deduction Rules from Truth Tables
• Intensional interpretations of functionals of finite type I
• Some Remarks on Proof-Theoretic Semantics
• Logic and structure.

This page was built for publication: Proof Terms for Generalized Natural Deduction