[Fwd: E Equational Theorem Prover 0.61 "North Tukvar" released]

[Massimo Dentico]

on news://comp.theory, 17 Apr 2001, Stephan Schulz wrote:
> 
> 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 schulz@informatik.tu-muenchen.de (Stephan Schulz)
> ----------------------------------------------------------------------------

Excerpt from the home page:

----------------------------------------------------------------------------
[...]

Performance

E 0.6 won the first place in the MIX category of the CASC-17 theorem proving
competition. We take this as a sign that E performs relatively well overall.
The latest version, E 0.61, is stronger still.

[...]
----------------------------------------------------------------------------

Bibliography at the bottom of the page.

Regards.

-- 
Massimo Dentico