A theorem prover called Weierstrass

View this page in Polish courtesy of   Andrey Fomin

This page reports on research conducted in 1996-99 with the partial support of NSF grant CCR-9528913, and on one continuation of that line of research.

The theorem prover Weierstrass was built by combining the symbolic computation facilities of Mathpert with an inference engine, earlier built for the theorem-prover Gentzen. These two components are intertwined quite intimately, rather than just "talking to" each other. The inference engine can take symbolic steps in a proof; the symbolic part can "simplify" propositions as well as mathematical expressions; the "simplification" can use the current assumptions from the logical framework; computation steps can use existing assumptions, or even make new ones.

The purpose of this research was to explore the relationship between logic and computation as they occur in the development of mathematical proofs.

The general plan for integrating logic and computation in a computer program had already been laid out, years before, and used in the design of Mathpert, a program for helping students learn algebra, precalculus, and calculus. Mathpert is now commercially available (see www.mathpert.com) . But Mathpert deals only with quantifier-free logic, since that is all that is required in algebra and calculus. Therefore, Weierstrass needed the extra apparatus of a theorem-prover, based on a backwards construction of a proof in Gentzen sequent calculus using unification to instantiate meta-variables for terms.

What remained to do after this integration was to demonstrate that these methods of integrating logic and computation actually work. This research was somewhat experimental in nature. The plan is simple: choose an area of mathematics, choose a well-known proof in that area, and see if Weierstrass can generate that proof , or can be made to generate it by adding some general-purpose meta-rules (rules governing the generation of proofs). Of course, if one has to add many meta-rules of a very specific nature before the result comes out, this is not satisfying. But it did not turn out that way.

Two quite different areas of mathematics were chosen for experimentation: analysis and number theory. To make a long story short, Weierstrass was able to generate several proofs involving epsilon-delta arguments (in analysis), and in number theory, it was able to prove the irrationality of e. Here is a somewhat longer version of the story:

In the area of analysis, I chose epsilon-delta proofs about continuity as the arena for experimentation. These are the first proofs we ask our students to do when they leave behind the purely computational beginnings of mathematics. Yet, until 1996, no theorem-prover could automatically generate a proof of, for example, the continuity of f(x) = x³, or f(x) = sin x. The reason is, that to prove these results involves some computational work: some manipulation of inequalities, some judicious factorization or use of trig identities, and good control of the transitivity law for inequalities. No previous program had incorporated both the logical and computational capabilities required for these proofs. This phase of the work was successful: about five meta-rules were needed to control the proof generation, and these rules were of a very general character (obviously not specific to epsilon-delta arguments). This work was presented at the conference on Artificial Intelligence and Symbolic Computation in September, 1998; see [43].

In the area of number theory, I chose the proof of irrationality of e. This is a proof sufficiently difficult that most people will not discover it for themselves. Weierstrass had to be given several more meta-rules before it could generate a proof. Again, those rules were not at all specific to this problem. The proof generated is much longer than the epsilon-delta proofs, requiring five pages to write out. It contains several interesting sub-proofs: a convergence estimate on an infinite series, using the comparison theorem, in which Weierstrass constructs a geometric series and frames as a subgoal the inequality needed to apply the comparison theorem. This inequality can’t be proved directly (at least not by Weierstrass) and is therefore attacked by mathematical induction. In the course of this induction, some simplification of expressions involving factorials is required. Finally, the key step involves an argument that a certain quantity is a positive integer, but has been estimated to be less than 1, contradicting the hypothesis that e is a quotient of integers. This work was presented at the Calculemus workshop of the Federated Logic Conferences in Trento (July 1999), and published in [44].

An interesting point is that after new meta-rules were added for number theory, the original proofs in analysis still could be generated. That is, there was no conflict between the meta-rules. One wonders if that would still be the case if 200 meta-rules for various subjects had been added. I think that in the (distant) future, a more systematic means of classifying mathematical knowledge (embodied in these meta-rules) according to subject, and applying rules relevant to the subject of the current goal, will be required.

A different strand of this research concerned the extension of Weierstrass to second-order logic. A new algorithm for unification in lambda-calculus with if-then-else was discovered (or invented) and some of its theoretical properties were proved, in a paper presented at CADE-15, the Conference on Automated Deduction in Lindau, July, 1998. It would be possible to implement this algorithm in a theorem-prover. Two years later, I did implement the algorithm in my prover Weierstrass, and then used Weierstrass to generate proofs using John McCarthy’s circumscription method. This work is described in [45].