Applications
E has been integrated into several other theorem provers. It is, with Vampire and SPASS, at the core of Isabelle's Sledgehammer strategy. E also is the reasoning engine in SInE and LEO-II and used as the clausification system for iProver.
Applications of E include reasoning on large ontologies, software verification, and software certification.
Read more about this topic: E Theorem Prover