Simplify Theorem Prover

The Eclipse Plugin for the Simplify Theorem Prover is found at http://kind/products/opensource/Simplify/simplify-eclipse/updates/

The source code is found in Subversion at
https://mobius.ucd.ie/repos/src/simplify

An archive of all binary executables for various platforms is found at http://kind/products/opensource/archives/Simplify1.5.5.zip

What is the future of Simplify?

Simplify was written by Greg Nelson and others at SRC. It is implemented in Modula-III. The only recent development on Simplify that has taken place is our port of it to Mac OS X. We do not plan on doing any development on Simplify, as the world of first-order theorem provers has changed quite a bit over the past decade or so. Instead, we are working on integrating ESC/Java3 with new-generation SMT-LIB provers.