On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
From MaRDI portal
(Redirected from Publication:265002)
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
Cites work
- scientific article; zbMATH DE number 1722654 (Why is no real title available?)
- scientific article; zbMATH DE number 2185662 (Why is no real title available?)
- scientific article; zbMATH DE number 5851813 (Why is no real title available?)
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 1324438 (Why is no real title available?)
- scientific article; zbMATH DE number 7393562 (Why is no real title available?)
- scientific article; zbMATH DE number 3271491 (Why is no real title available?)
- scientific article; zbMATH DE number 3358455 (Why is no real title available?)
- A new use of Friedman's translation: interactive realizability
- A semantics of evidence for classical arithmetic
- Ackermann's substitution method (remixed)
- Epsilon substitution method for elementary analysis
- Gentzen's Proof of Normalization for Natural Deduction
- Interactive learning-based realizability for Heyting arithmetic with \(\mathrm{EM}_1\)
- Interactive realizability for classical Peano arithmetic with Skolem axioms
- Interactive realizability for second-order Heyting arithmetic with EM1 and SK1
- Interactive realizers: a new approach to program extraction from nonconstructive proofs
- Lectures on the Curry-Howard isomorphism
- Non-determinism, non-termination and the strong normalization of System T
- Nondeterministic extensions of untyped \(\lambda\)-calculus
- On quantum lambda calculi: a foundational perspective
- On the interpretation of non-finitist proofs–Part II
- On weak completeness of intuitionistic predicate logic
- Probabilistic operational semantics for the lambda calculus
- Realizability and strong normalization for a Curry-Howard interpretation of HA + EM1
- The epsilon calculus and Herbrand complexity
Cited in
(14)- Quantum programming made easy
- A herbrandized functional interpretation of classical first-order logic
- Classical Logic with Mendler Induction
- Proofs of strong normalisation for second order classical natural deduction
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
- Disjunctive normal forms and local exceptions
- QPCF: higher-order languages and quantum circuits
- Game semantics and the geometry of backtracking: a new complexity analysis of interaction
- Proof nets for classical logic
- Realizability and strong normalization for a Curry-Howard interpretation of HA + EM1
- One-and-a-Halfth Order Terms: Curry-Howard and Incomplete Derivations
- On natural deduction for Herbrand constructive logics. I: Curry-Howard correspondence for Dummett's logic \(\mathsf {LC}\)
- Expansion trees with cut
- A short proof of the strong normalization of classical natural deduction with disjunction
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)
