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
Previous Page Next Page