E Equational Theorem Prover 0.61 "North Tukvar" released

[Stephan Schulz]

The E equational theorem prover version 0.61 "North Tukvar" has been
released.

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.61 has been carefully tested on all CNF problems of the TPTP
problem library, version 2.3.0, and showed no unexpected
behaviour. Some results are available from the web site. The prover
can produce checkable proof objects, a simple proof checker is
included in the distribution.

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 (with tweaking),
Solaris and HPUX. 

The system 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! ---------------------------------
   Please email me as address@hidden (Stephan Schulz)
----------------------------------------------------------------------------