Automated theorem proving Since the 1950s a fair amount of work has been done on trying to set up computer systems that can prove theorems automatically. But unlike systems such as Mathematica that emphasize explicit computation none of these efforts have ever achieved widespread success in mathematics. And indeed given my ideas in this section this now seems not particularly surprising. The first attempt at a general system for automated theorem proving was the 1956 Logic Theory Machine of Allen Newell and Herbert Simona program which tried to find proofs in basic logic by applying chains of possible axioms. But while the system was successful with a few simple theorems the searches it had to do rapidly became far too slow. And as the field of artificial intelligence developed over the next few years it became widely believed that what would be needed was a general system for imitating heuristics used in human thinking. Some work was nevertheless still done on applying results in mathematical logic to speed up the search process. And in 1963 Alan Robinson suggested the idea of resolution theorem proving, in which one constructs (\[Not] theorem \[Or] axioms), then typically writes this in conjunctive normal form and repeatedly applies rules like And[Or[Not[p], q], Or[p, q]]>q to try to reduce it to False, thereby proving given axioms that theorem is True. But after early enthusiasm it became clear that this approach could not be expected to make theorem proving easya point emphasized by the discovery of NP completeness in the early 1970s. Nevertheless, the approach was used with some success, particularly in proving that various mechanical and other engineering systems would behave as intendedalthough by the mid1980s such verification was more often done by systematic Boolean function methods (see page 1097). In the 1970s simple versions of the resolution method were incorporated into logic programming languages such as Prolog, but little in the way of mathematical theorem proving was done with them. A notable system under development since the 1970s is the BoyerMoore theorem prover Nqthm, which uses resolution together with methods related to induction to try to find proofs of statements in a version of Lisp. Another family of systems under development at Argonne National Laboratory since the 1960s are intended to find proofs in pure operator (equational) systems (predicate logic with equations). Typical of this effort was the Otter system started in the mid1980s, which uses the resolution method, together with a variety of ad hoc strategies that are mostly versions of the general ones for multiway systems in the previous note. The development of socalled unfailing completion algorithms (see page 1037) in the late 1980s made possible much more systematic automated theorem provers for pure operator systemswith a notable example being the Waldmeister system developed around 1996 by Arnim Buch and Thomas Hillenbrand. Ever since the 1970s I at various times investigated using automated theoremproving systems. But it always seemed that extensive human inputtypically from the creators of the systemwas needed to make such systems actually find nontrivial proofs. In the late 1990s, however, I decided to try the latest systems and was surprised to find that some of them could routinely produce proofs hundreds of steps long with little or no guidance. Almost any proof that was easy to do by hand almost always seemed to come out automatically in just a few steps. And the overall ability to do proofsat least in pure operator systemsseemed vastly to exceed that of any human. But as page 810 illustrates, long proofs produced in this way tend to be difficult to readin large part because they lack the higherlevel constructs that are typical in proofs created by humans. As I discuss on page 821, such lack of structure is in some respects inevitable. But at least for specific kinds of theorems in specific areas of mathematics it seems likely that more accessible proofs can be created if each step is allowed to involve sophisticated computations, say as done by Mathematica.



PAGE IMAGE
