My M.S. in Computer and Information Sciences was for Automated Thereom Proving, back in 1975.

UNIVERSITY OF MASSACHUSETTS, Amherst, MA 1973-1975

M.S., Computers and Information Science (Artificial Intelligence)

* Designed and coded parallel automated theorem prover

My advisor (Daniel Fishman) had an existence proof in his PhD dissertation. In constructively found an alogorithm and data structure which did automated theorem proving much much faster than any system in the world at the time – according to our simulations. There were no Massively Parallel Procfessors available to us in 1975. Xerox made a commercial product from our system, without payment or acknowledgment. But it was great fun, anyay.

Please allow me to give an introductory description, for those new to this topic.

Practical Foundations of Mathematics

Paul Taylor

1.7 Automated Deduction

There are mechanised approaches to algebra,

combinatorics, numerical analysis, etc , but this book

is not about those subjects, it is about logic: all we

can discuss in this section is the choreography of [non-unicode characters], and reinforce the importance of the

scope of variables and hypotheses. We cannot do the

creative part of mathematics, because the solution to

a problem in number theory, for example, may be

“simply” an ingenious observation about z(s) = ån =

1¥ n-s or counting points in a cube in Rn.

The steps which can be automated are the obvious ones,

in a technical sense: this literally means “in the

way” in Latin. It is obvious how to go through a

foreign airport, not because you know it intimately,

but because there are signs telling you where to turn

whenever you need them (you hope). This is also known

as exam technique: write down and exploit what you

already know. Whereas the box or sequent rules of

predicate calculus from the previous section are the

laws of the game of proof, the heuristics are hints on

the tactics. This section is based on teaching first

year informatics students to construct proofs on

paper. Of course this will also give some idea of how

to write a program to do it, but the strategy for

making choices when backtracking is needed raises

issues far outside the scope of this book [Pau92].

George Polya [Pol45] and Imre Lakatos [ Lak63] gave

two classic accounts of heuristics in mathematics,

using Euclidean geometry for examples. Polya’s advice

- make a plan and carry it out, compare your problem

with known theorems, etc - is extremely valuable to

help students of mathematics (and professionals) get

past the blank sheet of paper, but treats more

strategic aspects of proof than we can. An early

theorem prover was based on his methods of drawing

diagrams and formulating conjectures and

counterexamples; that this seems odd now shows both

the sophistication of modern proof theory and perhaps

also the danger of isolation from the traditional

instincts of mathematicians.

Nikolas de Bruijn’s AUTOMATH project (late 1960s) set

out to codify existing mathematical arguments, rather

than to find new theorems, and this remains the

research objective of automated reasoning. Johan van

Benthem Jutting (1977) translated Edmund Landau’s book

Foundations of Analysis into AUTOMATH and analysed the

ratio by which the text is magnified, which was

approximately constant from beginning to end. Similar

work has been done for other areas of mathematics.

There are certain dangers inherent in the

formalisation of mathematics. Systems of axioms

acquire a certain sanctity with age, and in the how of

churning out theorems we forget why we were studying

these conditions in the first place. Computer

languages suffer far more from this problem: nobody

would claim any intrinsic merit for FORTRAN or HTML,

but sheer weight of existing code keeps them in use.

Through the need for a standard - any standard - a

similar disaster could befall mathematics if set

theory were chosen. As with any programming, and also

with the verification of programs, far more detail is

required than is customary in mathematics. G. H. Hardy

(1940) claimed that there is no permanent place in the

world for ugly mathematics, but I have never seen a

program which is not ugly. Even when the mathematical

context and formal language are clear, we should not

perpetuate old proofs but instead look for new and

more perspicuous ones.

===========

[dB80]

Nikolas de Bruijn. A survey of the project Automath.

In Curry et al. [CSH80], pages 579-606.

[CSH80]

Haskell Curry, Jonathan Seldin, and Roger Hindley,

editors. To H.B. Curry: Essays on Combinatory Logic,

Lambda Calculus and Formalism. Academic Press, 1980.

[Har40]

G. H. Hardy. A Mathematician’s Apology. Cambridge

University Press, 1940. Reprinted 1992.

[Lak63]

Imre Lakatos. Proofs and refutations: the logic of

mathematical discovery. British Journal for the

Philosophy of Science, 14:1-25, 1963. Edited by John

Worrall and Elie Zahar, Cambridge University Press,

1976.

[Pau92]

Lawrence Paulson. Designing a theorem prover. In

Samson Abramsky et al., editors, Handbook of Logic in

Computer Science, pages 415-475. Oxford University

Press, 1992.

[Pol45]

George Polya. How to Solve It: a New Aspect of

Mathematical Method. Princeton University Press, 1945.

Re- published by Penguin, 1990.

## Re: Automated Theorem Proving

Well, there are those of us who use automated theorem provers, but don’t hold the computer’s hand to make them prove known results or to win competitions. Rather we use them in our research to discover new results.

I work quite a bit in the area of quasigroups and loops. I use Prover9, the successor to Otter developed by William McCune. My collaborators and I have used both Otter and Prover9 to solve some longstanding problems in the field.

To me, an important part of the process is “humanizing” the automated proof, that is, translating it into a form comprehensible by humans. This involves poring over the proof line by line, usually starting from the end. As I am reading it, I’ll come across a clause and think “Oh, that one follows immediately from such-and-such, so I don’t need to read Prover9’s proof”.

To give a concrete example, suppose I have managed to get Prover9 to prove something about Moufang loops. Such loops are diassociative, that is, any subloop generated by no more than two elements is associative. So if I am reading a proof and come across a two-variable instance of associativity, I don’t have to bother checking the proof of that particular clause. More generally, if the class of loops I am working on has known structure, I can use that in the translation process.

Eventually, with enough patience, I can get a proof that is not only checkable by humans (as any proof generated by this kind of software is, at least in principle), but is, in fact, comprehensible.

It is funny to use the word “reduce” here, but I like to think of it as “reducing” an entirely equational or first-order proof to higher order concepts. But occasionally there will be some part of a proof where it just isn’t possible to pull higher-order stuff out of a hat to get the result. In those cases, the best one can hope for is to write the steps as cleanly as possible. For instance, in our proof that every diassociative A-loop is Moufang, there is a lemma whose proof is just based on manipulating identities. It is a proof I still think it highly unlikely a human would have found (and certainly no human had in the 44 years the problem was open).