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 PROLOGlike 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:
Targeted Platforms: Software/Hardware Requirements:

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