On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
DOI10.1016/J.TCS.2016.02.028zbMATH Open1377.03050OpenAlexW2276824306MaRDI QIDQ265002FDOQ265002
Authors: Federico Aschieri, Margherita Zorzi 
Publication date: 1 April 2016
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2016.02.028
Recommendations
- On natural deduction for Herbrand constructive logics. I: Curry-Howard correspondence for Dummett's logic \(\mathsf {LC}\)
- A herbrandized functional interpretation of classical first-order logic
- Normalization theorems for full first order classical natural deduction
- Realizability and strong normalization for a Curry-Howard interpretation of HA + EM1
- New Curry-Howard terms for full linear logic
classical first-order logicCurry-Howard correspondencedelimited exceptionsHerbrand's theoremnatural deduction
Computational learning theory (68Q32) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) Classical first-order logic (03B10) Combinatory logic and lambda calculus (03B40)
Cites Work
- Epsilon substitution method for elementary analysis
- Ackermann's substitution method (remixed)
- Nondeterministic extensions of untyped \(\lambda\)-calculus
- Title not available (Why is that?)
- Interactive learning-based realizability for Heyting arithmetic with \(\mathrm{EM}_1\)
- Probabilistic operational semantics for the lambda calculus
- Interactive realizers: a new approach to program extraction from nonconstructive proofs
- Realizability and strong normalization for a Curry-Howard interpretation of HA + EM1
- On quantum lambda calculi: a foundational perspective
- Title not available (Why is that?)
- Title not available (Why is that?)
- Gentzen's Proof of Normalization for Natural Deduction
- Title not available (Why is that?)
- Title not available (Why is that?)
- Interactive realizability for classical Peano arithmetic with Skolem axioms
- A semantics of evidence for classical arithmetic
- Title not available (Why is that?)
- A new use of Friedman's translation: interactive realizability
- Non-determinism, non-termination and the strong normalization of System T
- Title not available (Why is that?)
- Title not available (Why is that?)
- On weak completeness of intuitionistic predicate logic
- Interactive realizability for second-order Heyting arithmetic with EM1 and SK1
- On the interpretation of non-finitist proofs–Part II
- The epsilon calculus and Herbrand complexity
- Lectures on the Curry-Howard isomorphism
Cited In (14)
- Proofs of strong normalisation for second order classical natural deduction
- Quantum programming made easy
- QPCF: higher-order languages and quantum circuits
- A herbrandized functional interpretation of classical first-order logic
- Disjunctive normal forms and local exceptions
- Game semantics and the geometry of backtracking: a new complexity analysis of interaction
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
- On natural deduction for Herbrand constructive logics. I: Curry-Howard correspondence for Dummett's logic \(\mathsf {LC}\)
- Realizability and strong normalization for a Curry-Howard interpretation of HA + EM1
- Classical Logic with Mendler Induction
- A short proof of the strong normalization of classical natural deduction with disjunction
- One-and-a-Halfth Order Terms: Curry-Howard and Incomplete Derivations
- Expansion trees with cut
- Proof nets for classical logic
This page was built for publication: On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q265002)
