Introduction

Watson is a general-purpose system for formal reasoning. It has been developed with applications to software development or verification in mind, but we have also considered applications in education or in pure mathematics. Earlier incarnations of the prover have been called EFTTP (which was a very different system) and Mark2 (which was similar though not identical to Watson; there are occasional references in the paper to differences between Mark2 and Watson: the best reference for Mark2 is the final report [16] of Holmes's first ARO grant).

Watson is a system for computer-supported reasoning by human beings rather than for automatic proof of theorems, though it does support the development of automated proof strategies.

Its logic is equational and rewriting plays a considerable role in the prover, though it is not a typical rewriting system. The properties of expressions defined by cases play an important role in its logic.

Watson supports a higher order logic, which is distinctive in being type-free: it is a $\lambda$-calculus equivalent to a variant of Quine's set theory ``New Foundations''. References for the theoretical aspects of the higher order logic include Quine's [25] and Jensen's [19] for the original systems of set theory and Holmes's [13], [15] and [17] for the development of the $\lambda$-calculus version.

This paper contains an overview of the mathematical foundations of Watson, followed by a discussion of the way these foundations are implemented in the prover, from the standpoint of a user. These two sections take up most of the paper. Two short sections, one on experiences with the prover and one on the relationships of the prover with other systems, complete the paper.

We are grateful for the support of the Army Research Office through three separate grants. The designer of the system (Holmes) is grateful to the other author for his work with the prover and for his work supervising students, and to the students for their efforts in learning and applying the system. Specifically we wish to thank the following students for their hours of work and dedication to this project: at the University of Idaho we thank Sol Espinosa, Fongshing Lam, Aaron Schneider, Kundala Shankar, and Minglong Wu; and at Boise State University we thank Michael Parvin for his excellent help. The University of Idaho research group owes a special thanks to Dr. Holmes for his continued support of our efforts and tremendous contribution to helping the students resolve problems arising in their work.

Source code and documentation for the Watson system are available at http://math.boisestate.edu/$\sim$holmes/proverpage.html.