Hilbert's programme and the search for automatic proof procedures

J.F. Adams, Vector fields on spheres, Ann. of Math 75(1962) pp. 603–632.
Article MathSciNet MATH Google Scholar
A. Baker, Contributions to the theory of Diophantine equations, Phil. Trans. Roy. Soc. A 263 (1968) pp. 173–208 and, for practical bounds, Linear forms in the logarithms of algebraic numbers (IV), Mathematika 15 (1968) pp. 204–216.
Article MATH Google Scholar
H. Davenport and K.F. Roth, Rational approximations to algebraic numbers, Mathematika 2 (1955) pp. 160–167.
Article MathSciNet MATH Google Scholar
B. Dreben, P. Andrews, S. Aandera, False lemmas in Herbrand, Bull. Ann. Math. Soc. 69 (1963) pp. 699–706.
Article MathSciNet MATH Google Scholar
G. Kreisel, Mathematical logic: what has it done for the philosophy of mathematics ? Bertrand Russel: Philosopher of the century, Allen and Unwin, London 1967, pp. 201–272.
Google Scholar
Survey of proof theory, J.S.L. 33 (1968) pp. 321–388.
Google Scholar
Church's thesis: a kind of reducibility axiom for constructive mathematics, to appear in the Proceeding of the conference on proof theory and intuitionism, Buffalo 1968.
Google Scholar
R.S. Lehman, On the difference II(x)-li(x), Acta arithmetica 11 (1966) pp. 397–410
MathSciNet MATH Google Scholar
J. Milnor, Somme consequences of a theorem of Bott, Ann. of Math. 68 (1958) pp. 444–449.
Article MathSciNet MATH Google Scholar
J.C. Shepherdson, Non-standard models for fragments of number theory, The theory of models, North Holland, Amsterdam, 1965, pp. 342–358.
MATH Google Scholar
D.B. Thompson, Dissertation, Stanford University, 1968.
Google Scholar
H.S. Vandiver, Fermat's last theorem. Its history and the known results concerning it, Am. Math. Monthly 53 (1946) pp. 555–578 and A supplementary note to a 1946 article on Fermat's last theorem, ibid. 60 (1953) pp. 164–167.
Article MathSciNet MATH Google Scholar
S. Winograd, How fast can computers add ? Scientific American 1968-(n^o) p. 93–100.
Google Scholar

Download references

Authors

G. Kreisel
View author publications
You can also search for this author in PubMed Google Scholar

Editor information

M. Laudet D. Lacombe L. Nolin M. Schützenberger

Rights and permissions

Reprints and permissions

Copyright information

About this paper

Cite this paper

Kreisel, G. (1970). Hilbert's programme and the search for automatic proof procedures. In: Laudet, M., Lacombe, D., Nolin, L., Schützenberger, M. (eds) Symposium on Automatic Demonstration. Lecture Notes in Mathematics, vol 125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0060629

Download citation

DOI: https://doi.org/10.1007/BFb0060629
Published: 23 August 2006
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-04914-2
Online ISBN: 978-3-540-36262-3
eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Hilbert's programme and the search for automatic proof procedures

Access this chapter

Preview

Bibliography