17 An Interactive Theorem-Proving Program

Rather, the program exists in a state of continual revision and extension, and that part of it which is running and yielding results at the moment is intended to form the nucleus of a much larger and more extensive automatic deduction system in the future. The program is being developed with a number of different questions and applications in mind. First of all, some of the present generation of deduction programs are already capable of proving the sort of theorem of an elementary mathematical theory that appears in the textbooks either as a basic theorem or standard exercise (sometimes as a'starred' exercise), and might reasonably be classified as'somewhat' tricky. We have in mind the theorems of algebra and number theory obtained by programs discussed by Wos, Robinson and Carson (1965), Wos et al. (1967), and Luckham (1968). In addition, it is reported by Guard et al. (1969) that an open problem in modular lattice theory was solved with the aid of an on-line program (and it is interesting to note that, with reference to the initial set of axioms and hypotheses, this seems not to be the most difficult theorem that has been proved by a program so far). We are thus motivated to ask if, by adding a flexible interactive facility to a good deduction program, it is possible to construct a system that would be useful in investigating some fairly basic mathematics.