E Theorem Prover

E Theorem Prover

E is a modern, high performance theorem prover for full first-order logic with equality. It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem proving competitions. E was developed by Stephan Schulz, originally in the Automated Reasoning Group at TU Munich.