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
- 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
- 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?)
- 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
(16)- Proof nets for classical logic
- QPCF: higher-order languages and quantum circuits
- A herbrandized functional interpretation of classical first-order logic
- Realizability and strong normalization for a Curry-Howard interpretation of HA + EM1
- On natural deduction for Herbrand constructive logics. I: Curry-Howard correspondence for Dummett's logic \(\mathsf {LC}\)
- One-and-a-Halfth Order Terms: Curry-Howard and Incomplete Derivations
- Proofs of strong normalisation for second order classical natural deduction
- A short proof of the strong normalization of classical natural deduction with disjunction
- Game semantics and the geometry of backtracking: a new complexity analysis of interaction
- Quantum programming made easy
- Expansion trees with cut
- Disjunctive normal forms and local exceptions
- Classical Logic with Mendler Induction
- On natural deduction for Herbrand constructive logics. II: Curry-Howard correspondence for Markov's principle in first-order logic and arithmetic
- A typed parallel -calculus via 1-depth intermediate proofs
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
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)
