E 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 diffcult problems.

Current Version:   0.32 License Type:   GPL

Home Site: http://wwwjessen.informatik.tu-muenchen.de/~schulz/WORK/eprover.html Source Code Availability: Yes Available Binary Packages: Debian Package: No RedHat RPM Package: No Other Packages: No Targeted Platforms: UNIX-like systems. Tested on Linux/Intel, Linux/SPARC, SunOS, Solarix, HPUX Software/Hardware Requirements: tar, gnuzip, make, gcc (or other ANSI C compiler), ar

Other Links: None Mailing Lists/USENET News Groups: None User Comments: None See A Screen Shot? (Not Yet)

  SAL Home   |   Mathematics   |   Misc