This is no longer the top level page; a new implementation, now called Watson, can be found here on the new Watson page.

Attention Michael Parvin: here is the script parvin_programs.mk2 and the background theory file preprograms.wthy you need to run the script. The script is far from complete, but you can start looking at it to get an idea what my approach is.

I am developing an equational interactive theorem prover called Mark2. The SML source code can be viewed as a Postscript file here or it can be seen as plain text here . IMPORTANT UPDATE INFORMATION here . If you like living dangerously, I will sometimes post draft versions of the source as well. If you plan to try to learn to use Mark2, please notify me at so that I can notify you in turn about upgrades (this is software under construction). Theory files are available from me on request. More or less complete documentation, including the documents posted here earlier in revised form and much new material, is available as of Sept. 21 as Postscript or as LaTeX source. This work is supported by a grant from the Army Research Office.

New: there is an attempt (automatically generated using latex2html) at HTML documentation of the prover. Take a look.

Another grant from the Army Research Office supports a separate project using Mark2 at the University of Idaho. You can find out about it here. A paper on the logic EFT which underlay an old version of the prover and is still relevant to some theories implemented under the current prover is available.

I think that I fulfilled my obligation to provide better documentation in part, but the Sept. 21 documents certainly need expansion (e.g., more examples, more discussion of programming in the tactic language, and a discussion of the underlying logical approach). The version notes file will also contain information on documentation updates.

Some useful scripts (you should get all of them, because some call others).

The final technical report of the first grant from the Army Research Office is here.