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.