by The E equational theorem prover version 0.5 "Phuguri" has been
released.
Version 0.5 participated in two categories of the 1999 CADE ATP System
Competition (http://www.cs.jcu.edu.au/~tptp/CASC-16/, results are
mirrored at http://wwwjessen.informatik.tu-muenchen.de/~tptp/CASC-16/)
and won fourth place in both. It won two of the five subdivisions of
the prestigious MIX category. A prerelease version of E 0.5 was a
major component of the E-SETHEO system that won MIX.
E is a a purely equational theorem prover for clausal logic with
equality. Thus, you can specify a mathematical problem (e.g. a
mathematical puzzle), a (small) piece of program code or some hardware
elements in clausal logic (using rules of the form "If A and B and C
then D or E or F" in a PROLOG-like syntax), and try to have the system
prove certain properties of the described structure. Be warned that
this can consume inane (in fact, theoretically unlimited) amounts of
CPU time and memory for difficult problems.
E 0.5 has been tested on all 3334 CNF problems of the TPTP problem
library, version 2.2.0, and showed no unexpected behaviour. Some
results are available from the web site.
E is available as a source distribution for UNIX-variants. It installs
cleanly under all UNIX variants I could get my hands on: Various
versions of GNU/Linux for Intel and SPARC, SunOS, Solaris and HPUX.
E is distributed under the GNU General Public License.
You can find the source distribution and additional information at
http://wwwjessen.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
Our servers are usually rebooted Monday mornings between 3:30 and 4:00
ME(S)Z, and may be unavailable during this time.
Have fun!
Stephan
-------------------------- It can be done! ---------------------------------
---------------------------------------------------------------------------