**"The proposition took me completely by surprise"**

(Dr. Watson in the Hound of the Baskervilles)

# The Watson Theorem Prover

I was at one time developing an equational interactive theorem prover called Watson
(before 1998, Mark2). The SML 93 source code can be seen here (somewhat out of date), and the Moscow ML/SML
96 source here. The Moscow ML
version is the one that one should use if one wants to explore this.
I also created a version using combinatory logic (and relying
on manipulations of combinators throughout); the source is here
and the manual is here. This version (CL Watson) displays lambda-terms
normally, but you can view the hideous combinators that it generates
if you like that sort of thing! I think that this version is bound tobe of more theoretical interest than practical interest, but one can do things with it. The intellectual interest arises from the fact that everything is being implemented on a very small minimal basis of concepts (which is not true in Watson, whose metatheory is rather baroque).

A different theorem proving software, Marcel, based on sequent calculus
rather than equational reasoning, but also based on a version of
Quine's New Foundations as its higher order logic (essentially the
same as the logic of Watson) is found here (ML source) and here (PDF documentation). I am hoping to integrate the Watson approach to equational reasoning with the sequent calculus approach in this system.

There is on-line
documentation for the prover here. This is probably the best resource for figuring out what is going on here! Here is
a paper about Watson.

Latest official version of the source posted Feb. 18, 2001, and dated
Feb. 18, 2001. This version has some new behavior dictated by the
needs of a GUI under development: there is a note on these changes in
the online command reference.

Here is a file proverpackage.tar.gz which contains
an essentially complete release of the prover, with source files,
documentation, and lots of theory files. Newly updated Feb. 18,
2001.

Draft versions of the prover not yet officially adopted may be found
here. This is currently the same
as the official version (Feb. 18).

This work was supported by a grant from the Army Research Office (the
second so far). Another grant from the Army Research Office
supported a separate project using Mark2 at the University
of Idaho.

Watson scripts are found here.

A technical report on Mark2, an earlier version of Watson, is found here.
Sometime I may try to resurrect some of this. Ideas from the Watson rewrite system are currently being added to Lestrade.

## Other theorem proving systems

If you'd like to find web resources on other theorem proving systems,
here is a
list of systems for computer implementation of mathematics
(including but not limited to theorem provers) prepared by Freek Wiedijk, whose implementation of
Automath deserves notice.