The Next Generation of Interactive Theorem Provers
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).
KeywordsTheorem Prover Elementary Geometry Current Goal Interactive Proof Interactive Theorem Prover
Unable to display preview. Download preview PDF.
- 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
- Suppes, P. Computer-assisted instruction at Stanford. In Man and computer. Basel: Karger, 1972.Google Scholar
- 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
- Suppes, P., and Binford, F. Experimental teaching of mathematical logic in the elementary school. The Arithmetic Teacher, 1965, 12, 187–195.Google Scholar