"The proposition took me completely by surprise"

(Dr. Watson in the Hound of the Baskervilles)

The Watson Theorem Prover

I am 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 usually the freshest.

NEW: I'm preparing a version using combinatory logic (and relying on manipulations of combinators throughout); the source is here and the manual is here (Postscript) or here (LaTeX source). 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).

NEW: A different theorem proving software, 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.

Version notes for Watson are found at the beginning of the source code. Documentation, headed by a draft of a paper on the prover, was found here but has now been removed for copyright reasons (the paper will appear in the Journal of Automated Reasoning). There is on-line documentation for the prover here.

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 is supported by a grant from the Army Research Office (the second so far). Another grant from the Army Research Office (recently ended) has supported a separate project using Mark2 at the University of Idaho. You could once find out about it here. Since the previous link seems to be broken, I also provide this, a link to a student's site at UI with good connectivity to resources there.

Here are the Watson scripts (overhauled Dec. 6, 2000)

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.

Precursors of this system

Here is a page with discussion of the differences between Watson and Mark2. (This is quite old; it goes back to the time of the first version of Watson (summer 1998).)

A paper on the logic EFT which underlay an old version of the prover and is still relevant to some aspects of the current prover is available. The quite different prover EFTTP described in this paper can be obtained from the author; it is a toy and embodies a very different approach from that eventually taken in Watson, though the Watson approaches to term navigation and to tactic programming are already seen. A better paper on the logic of Watson was presented at TPHOLs 2000, and is found in the proceedings of that conference (see my c.v. for reference).

The final technical report of the first grant from the Army Research Office is here. It discusses the last release of Mark2.

Here is the old Mark2 page and the Mark2 scripts.

Randall Holmes Home Page