28

D.W. LOVELAND

when theorems are retained after conversion to rewrite rules (at

the discretion of the user). Retention of previously established

results is natural and common to most systems in some degree.

The state-of-the-art in learning within a mathematics context

occurs in concept formation and theorem generation in the work

of Doug Lenat [Lel] (also see this volume).

We conclude the paper with some remarks regarding non-

standard applications of automated theorem provers, that is, their

use outside the role of proving theorems of interest to the

mathematical community. An area receiving considerable atten-

tion over the last decade is formal program verification, where a

program is "proved" correct by proving a series of "verification

conditions" which are propositions_ relating a portion of code to

formal specifications of the program. Although the logician Turing

had anticipated the basic concept, John McCarthy [Mel] and

Robert Floyd [Fll] are the direct creators of the methodology of

program verification. The methodology of verification was

advanced by the important early contributions of Naur [Nal] and

Hoare [Hol], the latter providing a specific formalization of the

program semantics of an ALGOL (or PASCAL) type programming

language via an axiom set. The first actual implementation of a

program verifier was that of James King [Kil] completed in 1969.

Extensive hand computed formal verification of modest-sized pro-

grams by Ralph London about 1970 stimulated the development of

more than one verification project. Since 1970 there have been

numerous programs which had program verification as their pri-

mary or secondary goal {e.g. the Boyer-Moore System mentioned

earlier). This relative intensity occurred because of the real need

to find ways of locating non-trivial errors in programs, and ideally