No-counterexample interpretation et sp\'{e}cification des th\'{e}or\`{e}mes de l'arithm\'{e}tique
From MaRDI portal
Publication:6475008
arXivmath/0501476MaRDI QIDQ6475008FDOQ6475008
Authors: Denis Bonnay 
Publication date: 26 January 2005
Abstract: This paper presents two different ways of extracting the computational content of formal proofs in arithmetic. The first one corresponds to Kreisel's No-counterexample Interpretation. based on Ackermann consistency proof. We show the link with recent work by Krivine on classical realizability. Finally, we discuss the various degrees of modularity of both approaches.
This page was built for publication: No-counterexample interpretation et sp\'{e}cification des th\'{e}or\`{e}mes de l'arithm\'{e}tique
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6475008)
