I have worked in mathematical logic, theoretical computer science, minimal surfaces, automated deduction, and written a large software program to help students learn mathematics. I continue to maintain an active interest in all those subjects.
Mathematical Logic and Theoretical Computer Science
My work in mathematical logic is on the metamathematics of constructive mathematics. This work began with my thesis (Stanford 1972) and culminated with my book Foundations of Constructive Mathematics. The formal systems developed for constructive mathematics, especially those known as "type theories", turned out to be of interest in theoretical computer science as well. Indeed I think that most of the readers of Foundations of Constructive Mathematics have been computer scientists.
While at Stanford, I was exposed to this beautiful and classical area of mathematics. As I worked on constructive mathematics, I used minimal surfaces as an example to help me understand the implications of the constructivist approach. Some of the questions I ran into led me to new results, and for some years (1977-1979) I was fascinated with the subject and worked on it to the virtual exclusion of my other research interests. In 1980 I put the subject aside in favor of writing the book mentioned above on constructive mathematics. Twenty years later I returned to the subject to finish solving the problem I was working on in 1980. The resulting long paper is posted on this website (see the publications page) but still not submitted for publication; most of its sections have been checked by experts, but one section remains to be verified by others.
In 1983, I learned to program in Prolog, and used it to implement many of the logical systems I had studied as a logician. Due to the magic of Prolog, some of these definitions became functional theorem-provers or proof checkers. I wrote an interesting theorem-proving program based on Gentzen's sequent calculus, which I named after Gentzen. Later, as I began to develop MathXpert, I focussed my attention on the relations between logic and computation. For more details: Description of Research in Automated Deduction from 1983-1995.
Based on a theory I developed about the right way to combine logic and computation, I was able to give my prover Gentzen some ability to compute with algebra and with inequalities. This new prover I called Weierstrass. Its implementation made use of some of the computational code from MathXpert. To demonstrate that logic and computation had successfully been combined in the same program, I used Weierstrass to find epsilon-delta proofs about continuity, such as the continuity of specific functions like x3 or sin x. Before this, no program had been able to prove the continuity of any specific non-linear function, and it was regarded as a good piece of work to prove the continuity of a linear function. To demonstrate the successful combination of logic and computation in another area of mathematics, I turned to number theory. Weierstrass was able to find a proof of the irrationality of the number e. For more details: Description of Research in Automated Deduction from 1996-2001
Another line of research I have pursued in automated deduction has to do with extensions of unification to second-order unification, or more recently, lambda unification. These are techniques for having a program come up with an appropriate definition of a function as required to complete a proof. For example, if we need a function f that satisfies f(0) = 1 and f(1) = 3, how is a computer program supposed to come up with f? Since sets can be considered as Boolean-valued functions, the problem of coming up with appropriate function definitions includes the problem of defining sets that may be required to complete proofs. In second-order logic, there are systems for proving theorems involving sets and/or functions, and much of mathematics is more naturally formalized in simple second-order systems than in full-blown set theory. In conference presentations I gave a new algorithm for second-order unification and proved some theorems about its behavior , implemented it in a theorem-proving program, and demonstrated the effectiveness of that program by using it to solve some problems in artificial intelligence using John McCarthy's method of circumscription .
While on leave in 2000, I collaborated with Larry Wos, the author of several books on theorem-proving with the program Otter. We used Otter to prove lemmas for us, and we wrote a joint paper  with Robert Veroff on double-negation elimination in various propositional logics. To state the point clearly: we proved new theorems in logic, publishable in logic journals, with the aid of a theorem-proving program.
Around 2002, I started to write and work with a new theorem prover, Otter-lambda. My "second-order unification" evolved into an untyped unification I called "lambda unification", and I formulated "lambda logic" in  to give a logical foundation to what the prover Otter-lambda does. This work was supported by a grant from the National Science Foundation from 2002-2006. There is now a website devoted to this project. To demonstrate the value of this approach, I showed how to use Otter-lambda to find proofs by mathematical induction. A paper describing the work on induction  has been accepted by the Journal of Automated Reasoning, and will appear in the second half of 2006.
MathXpert not only has the ability to carry out individual steps on command, but it also contains a sophisticated set of rules enabling it to solve almost any textbook problem in the subjects mentioned. It uses this ability to provide assistance to the student who does not know what to do. It can, if necessary, generate a complete step-by-step solution for the student to examine.
In 2004, I re-acquired the rights to MathXpert from the company that owns it. It is now available for download and purchase at www.HelpWithMath.com
I have only one paper in this category, but it doesn't fit in any of the other four categories. I once had a good Mexican dinner at which John McCarthy was the host. He asked whether an equilateral triangle could have all three of its corners at points in the plane with integer coordinates. This was a teaser: he already knew the answer and a more general theorem. But he did not know which triangles are similar to a triangle with all corners on integer coordinates in n-space, even for n=3. On the drive home I used the fact that every integer is the sum of four squares to prove that n=5 is as far as you have to look: if the triangle isn't "embeddable" in 5-space increasing n won't help. But it took quaternions to settle the cases n=3 and n=4. This work appeared in  and should in principle be accessible to a good high-school student.