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.