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! ---------------------------------

---------------------------------------------------------------------------