Interactive realizability for classical Peano arithmetic with Skolem axioms
From MaRDI portal
Publication:4649536
Recommendations
- Interactive realizability for second-order Heyting arithmetic with EM1 and SK1
- Interactive realizability and the elimination of Skolem functions in Peano arithmetic
- Interactive learning-based realizability for Heyting arithmetic with \(\mathrm{EM}_1\)
- Interactive realizers: a new approach to program extraction from nonconstructive proofs
- Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1
Cited in
(12)- A constructive analysis of learning in Peano arithmetic
- On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
- scientific article; zbMATH DE number 7393562 (Why is no real title available?)
- Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1
- On natural deduction for Herbrand constructive logics. I: Curry-Howard correspondence for Dummett's logic \(\mathsf {LC}\)
- Interactive realizers: a new approach to program extraction from nonconstructive proofs
- Interactive realizability for second-order Heyting arithmetic with EM1 and SK1
- Interpreting a classical geometric proof with interactive realizability
- Interactive learning based realizability and 1-backtracking games
- A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract)
- Interactive learning-based realizability for Heyting arithmetic with \(\mathrm{EM}_1\)
- Interactive realizability and the elimination of Skolem functions in Peano arithmetic
This page was built for publication: Interactive realizability for classical Peano arithmetic with Skolem axioms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4649536)
