摘要
当代“证明挖掘”研究的历史根源于格奥尔格·克莱瑟的“挖掘证明”研究纲领。在本文中,我们详细阐述克莱瑟这一想法对应用证明论仍在持续的巨大影响,并且讨论证明挖掘的一些逻辑方面。
The contemporary“proof mining”paradigm has its historical roots in Georg Kreisel’s program of“unwinding of proofs”.In this paper we elaborate on the tremendous influence Kreisel’s ideas have had and still have on this applied reorientation of proof theory and discuss some logical aspects of“proof mining”.
作者
乌利齐·克伦巴赫
Ulrich Kohlenbach(Department of Mathematics,Technische Universität Darmstadt)
出处
《逻辑学研究》
2023年第3期1-35,共35页
Studies in Logic