The Next Generation of Interactive Theorem Provers

  • Patrick Suppes
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


Prior to discussing what I see as desirable and achievable features of the next generation of interactive theorem provers, I want to say something about the history of my own work and that of my colleagues, which forms the basis for the view of the future I sketch in the remainder of this paper. Simple uses of an interactive theorem prover for the teaching of elementary logic began more than twenty years ago. I remember well our first demonstrations with elementary-school children in 1963. For a number of years we concentrated on teaching elementary logic and algebra to bright elementary- and middle-school children. We felt at the time that this was the right level of difficulty to reach for in terms of computer capacity and resources that could be devoted to the endeavor. All of this early work was done on one of the low-serial-number PDP-l’s, which John McCarthy and I jointly purchased from grants at Stanford in 1963. This early work has been described in (1965) and (1972).


Theorem Prover Elementary Geometry Current Goal Interactive Proof Interactive Theorem Prover 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. McDonald, J., and Suppes, P. Student use of an interactive theorem prover. In W. W. Bledsoe and D. W. Loveland (Eds.), Automated theorem proving: After 25 years. Providence, R.I.: American Mathematical Society, 1984.Google Scholar
  2. Suppes, P. Introduction to logic. New York: Van Nostrand, 1957.zbMATHGoogle Scholar
  3. Suppes, P. Axiomatic set theory. New York: Van Nostrand, 1960. Slightly revised edition published by Dover, New York, 1972.zbMATHGoogle Scholar
  4. Suppes, P. Computer-assisted instruction at Stanford. In Man and computer. Basel: Karger, 1972.Google Scholar
  5. Suppes, P. (Ed.), Universitxy-level computer-assisted instruction at Stanford: 1968–1980. Stanford, Calif.: Stanford University, Institute for Mathematical Studies in the Social Sciences, 1981.Google Scholar
  6. Suppes, P., and Binford, F. Experimental teaching of mathematical logic in the elementary school. The Arithmetic Teacher, 1965, 12, 187–195.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Patrick Suppes
    • 1
  1. 1.Stanford UniversityUSA

Personalised recommendations