Geodesic
From Foundations to Science: Justifying and Unwinding Proofs
Zbornik radova, Tome 2 (1977) no. 10, p. 63

Voir la notice de l'article provenant de la source eLibrary of Mathematical Institute of the Serbian Academy of Sciences and Arts

The first part of this paper recapitulates the general scheme of using techniques developed for discredited foundational aims; specifically, proof theoretic techniques developed for carrying out HiIbert's programme. Since this programme relies on formalization, that is, mechanization, an obvious use is in the mechanical 'handling' of proofs. - The second part of the paper considers three different kinds of 'handling:' finding, checking and unwinding (transforming) proofs. The principal, generally neglected conclusion is that mechanical unwinding presents the most promising application of proof theoretic techniques; particularly where the passage from the informal proof considered to a formalization of its relevant features is not particularly problematic. Examples of such cases are proposed. 
@article{ZR_1977_2_10_a4,
     author = {Georg Kreisel},
     title = {From {Foundations} to {Science:} {Justifying} and {Unwinding} {Proofs}},
     journal = {Zbornik radova},
     pages = {63 },
     publisher = {mathdoc},
     volume = {2},
     number = {10},
     year = {1977},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/ZR_1977_2_10_a4/}
}
TY  - JOUR
AU  - Georg Kreisel
TI  - From Foundations to Science: Justifying and Unwinding Proofs
JO  - Zbornik radova
PY  - 1977
SP  - 63 
VL  - 2
IS  - 10
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/ZR_1977_2_10_a4/
LA  - en
ID  - ZR_1977_2_10_a4
ER  - 
%0 Journal Article
%A Georg Kreisel
%T From Foundations to Science: Justifying and Unwinding Proofs
%J Zbornik radova
%D 1977
%P 63 
%V 2
%N 10
%I mathdoc
%U http://geodesic.mathdoc.fr/item/ZR_1977_2_10_a4/
%G en
%F ZR_1977_2_10_a4
Georg Kreisel. From Foundations to Science: Justifying and Unwinding Proofs. Zbornik radova, Tome 2 (1977) no. 10, p. 63 . http://geodesic.mathdoc.fr/item/ZR_1977_2_10_a4/