算术定理的无反例解释与具体化
No-counterexample interpretation et spécification des théorèmes de l'arithmétique
摘要：
本文提出了两种不同的方法来提取算术形式证明的计算内容。第一个对应于Kreisel的无反例解释。基于Ackermann一致性证明我们显示的联系与最近的工作Krivine经典的可实现性。最后，我们讨论了这两种方法的模块化程度。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
