Mathematical texts consist not only of definitions and theorems but also of proof techniques. To formalize mathematics one must formalize these methods as well. In this is done by expressing proof methods as programs in the ML programming language. We think of ML as formalizing the computational part of the metalanguage. One of the research topics of our group concerns the complete formalization of the metalanguage (see [Knoblock 86]).

This approach to formalization brings with it a method of mechanizing
reasoning in Nuprl
, for as users write more and more elaborate proof--building
methods the system can do more of the work of finding proofs.
This approach to ``theorem proving'' continues the tradition of our
earlier work on
PL/CV [Constable, Johnson, & Eichenlaub 82,Constable & O'Donnell 78] and follows in the spirit of the
Edinburgh LCF project,
which spawned ML. The style of formalization
extends the AUTOMATH [deBruijn 80] approach
to presenting proofs, an approach which relies mainly on a very
high--level language for writing proofs. As more and more complex
tactics are built this line of research comes closer to the mainstream
work in * automated theorem proving*
[Andrews 71,Bibel 80,Bledsoe 77,Boyer & Moore 79,Loveland 78,Weyhrauch 80,Wos et al. 84].
It is conceivable that one
would write a tactic which is so ambitious that it would be classified
as a ``theorem prover''.

Although we have written many useful tactics and although the system
provides a nontrivial level of deductive support, none of our
methods can presently be classified as theorem provers. We are, however,
exploring some interesting new methods such as analogy tactics and
``expert reasoners'' which we think will be contributions to the subject of
* automated reasoning*.

Thu Sep 14 08:45:18 EDT 1995