Boyer and Moore: induction without human hints

In August 1973, at IJCAI in Stanford, Robert Boyer and J Strother Moore of the University of Edinburgh described a program that proves theorems about recursive LISP functions by mathematical induction on its own; among them, that REVERSE is its own inverse and that a particular sorting program is correct. On an ICL 4130 each theorem took 8 seconds on average.

The program takes a LISP expression, runs it in an interpreter and derives an induction formula from the way the interpreter fails; to this it adds simple rewrite rules of LISP and a heuristic for generalising the theorem. According to the paper, the user supplies nothing but the function definitions. The 8-second average was measured on an ICL 4130 in POP-2. Appendix B lists the theorems proved. The sorting claim has a caveat. The abstract says that a particular SORT program is correct; the body gives only that the output is ordered as its example; and Appendix B lists, among the theorems proved, that the number of occurrences of an element is the same in the input and in the output of SORT. In his archive of 2018 J Strother Moore writes that the correctness of insertion sort was stated as two theorems, ordered output and preserved occurrences, that the second is not proved in the listing of 18 July 1973 he has (it is marked as a challenge) and that it is listed among the successful theorems in his dissertation some months later. The record does not decide whether the program had proved the second theorem before the paper went to print. What the record does not claim: how many theorems the appendix holds; the paper does not count them.