|
E is a modern, high performance theorem prover for first-order logic with equality. The system is based on the equational superposition calculus and implemented in C.
It is available under the GNU GPL, portable to most UNIX dialects, and can be downloaded from the home page linked below.
External link
|
