SAL Home MATH Misc


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:

Source Code Availability:


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:

Mailing Lists/USENET News Groups:


User Comments:

  • None

See A Screen Shot? (Not Yet)

  SAL Home   |   Mathematics   |   Misc

Comments? SAL@KachinaTech.COM
Copyright © 1995-2001 by Herng-Jeng Jou
Copyright © 1997-2001 by Kachina Technologies, Inc.
All rights reserved.