Interactive realizability for classical Peano arithmetic with Skolem axioms
From MaRDI portal
Publication:4649536
DOI10.4230/LIPICS.CSL.2012.31zbMATH Open1252.03133OpenAlexW1825162208MaRDI QIDQ4649536FDOQ4649536
Authors: Federico Aschieri 
Publication date: 22 November 2012
Full work available at URL: https://hal.inria.fr/hal-00685360
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
- Title not available (Why is that?)
- On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
- 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)
