克莱瑟的“重心转移”及当代证明挖掘

Kreisel’s“Shift of Emphasis”and Contemporary Proof Mining

当代“证明挖掘”研究的历史根源于格奥尔格·克莱瑟的“挖掘证明”研究纲领。在本文中,我们详细阐述克莱瑟这一想法对应用证明论仍在持续的巨大影响,并且讨论证明挖掘的一些逻辑方面。

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”.