# E (theorem prover)

**E** is a high performance theorem prover for full first-order logic with equality.^{[1]} 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 is developed by Stephan Schulz, originally in the *Automated Reasoning Group* at TU Munich, now at Baden-Württemberg Cooperative State University Stuttgart.

## System

The system is based on the equational superposition calculus. In contrast to most other current provers, the implementation actually uses a purely equational paradigm, and simulates non-equational inferences via appropriate equality inferences. Significant innovations include shared term rewriting (where many possible equational simplifications are carried out in a single operation),^{[2]} several efficient term indexing data structures for speeding up inferences, advanced inference literal selection strategies, and various uses of machine learning techniques to improve the search behaviour.^{[2]}^{[3]}^{[4]} Since version 2.0, E supports many-sorted logic. ^{[5]}

E is implemented in C and portable to most UNIX variants and the Cygwin environment. It is available under the GNU GPL.^{[6]}

## Competitions

The prover has consistently performed well in the CADE ATP System Competition, winning the CNF/MIX category in 2000 and finishing among the top systems ever since.^{[7]} In 2008 it came in second place.^{[8]} In 2009 it won second place in the FOF (full first order logic) and UEQ (unit equational logic) categories and third place (after two versions of Vampire) in CNF (clausal logic).^{[9]} It repeated the performance in FOF and CNF in 2010, and won a special award as "overall best" system.^{[10]} In the 2011 CASC-23 E won the CNF division and achieved second places in UEQ and LTB.^{[11]}

## Applications

E has been integrated into several other theorem provers. It is, with Vampire, SPASS, CVC4, and Z3, at the core of Isabelle's *Sledgehammer* strategy.^{[12]}^{[13]} E also is the reasoning engine in SInE^{[14]} and LEO-II^{[15]} and used as the clausification system for iProver.^{[16]}

Applications of E include reasoning on large ontologies,^{[17]} software verification,^{[18]} and software certification.^{[19]}

## References

**^**Schulz, Stephan (2002). "E - A Brainiac Theorem Prover".*Journal of AI Communications*.**15**(2/3): 111–126.- ^
^{a}^{b}Schulz, Stephan (2008). "Entrants System Descriptions: E 1.0pre and EP 1.0pre". Retrieved 24 March 2009. **^**Schulz, Stephan (2004). "System Description: E 0.81".*Proceedings of the 2nd International Joint Conference on Automated Reasoning*. Lecture Notes in Computer Science. Springer. LNAI 3097: 223–228. doi:10.1007/978-3-540-25984-8_15. ISBN 978-3-540-22345-0.**^**Schulz, Stephan (2001). "Learning Search Control Knowledge for Equational Theorem Proving".*Proceedings of the Joint German/Austrian Conference on Artificial Intelligence (KI-2001)*. Lecture Notes in Computer Science. Springer. LNAI 2174: 320–334. doi:10.1007/3-540-45422-5_23. ISBN 978-3-540-42612-7.**^**"news on E's website". Retrieved 10 July 2017.**^**Schulz, Stephan (2008). "The E Equational Theorem Prover". Retrieved 24 March 2009.**^**Sutcliffe, Geoff. "The CADE ATP System Competition". Archived from the original on 2 March 2009. Retrieved 24 March 2009.**^**FOF division of CASC in 2008**^**Sutcliffe, Geoff (2009). "The 4th IJCAR Automated Theorem Proving System Competition--CASC-J4".*AI Communications*.**22**(1): 59–72. Retrieved 16 December 2009.**^**Sutcliffe, Geoff (2010). "The CADE ATP System Competition". University of Miami. Retrieved 20 July 2010.**^**Sutcliffe, Geoff (2011). "The CADE ATP System Competition". University of Miami. Retrieved 14 August 2011.**^**Paulson, Lawrence C. (2008). "Automation for Interactive Proof: Techniques, Lessons and Prospects" (PDF).*Tools and Techniques for Verification of System Infrastructure - A Festschrift in Honour of Professor Michael J. C. Gordon FRS*: 29–30. Retrieved 19 December 2009.**^**Meng, Jia; Lawrence C. Paulson (2004). "Experiments on Supporting Interactive Proof Using Resolution".*LNCS*. Lecture Notes in Computer Science. Springer.**3097**: 372–384. CiteSeerX 10.1.1.62.5009. doi:10.1007/978-3-540-25984-8_28. ISBN 978-3-540-22345-0.**^**Sutcliffe, Geoff; et al. (2009).*The 4th IJCAR ATP System Competition*(PDF). Retrieved 18 December 2009.**^**Benzmüller, Christoph; Lawrence C. Paulson; Frank Theiss; Arnaud Fietzke (2008). "LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)" (PDF).*LNCS*. Lecture Notes in Computer Science. 4th International Joint Conference on Automated Reasoning, IJCAR 2008 Sydney, Australia: Springer.**5195**: 162–170. doi:10.1007/978-3-540-71070-7_14. ISBN 978-3-540-71069-1. Archived from the original (PDF) on 15 June 2011. Retrieved 20 December 2009.**^**Korovin, Konstantin (2008). "iProver—an instantiation-based theorem prover for first-order logic (system description)" (PDF).*LNCS*. Lecture Notes in Computer Science. Springer.**5195**: 292–298. doi:10.1007/978-3-540-71070-7_24. ISBN 978-3-540-71069-1. Retrieved 18 December 2009.^{[permanent dead link]}**^**Ramachandran, Deepak; Pace Reagan; Keith Goolsbery (2005). "First-Orderized ResearchCyc : Expressivity and Efficiency in a Common-Sense Ontology" (PDF).*AAAI Workshop on Contexts and Ontologies: Theory, Practice and Applications*. AAAI.**^**Ranise, Silvio; David Déharbe (2003). "Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs".*ENTCS*. 4th International Workshop on First-Order Theorem Proving: Elsevier.**86**(1): 109–119. doi:10.1016/S1571-0661(04)80656-X. Archived from the original on 9 September 2012. Retrieved 18 December 2009.**^**Denney, Ewen; Bernd Fischer; Johan Schumann (2006). "An Empirical Evaluation of Automated Theorem Provers in Software Certification".*International Journal on Artificial Intelligence Tools*.**15**(1): 81–107. CiteSeerX 10.1.1.163.4861. doi:10.1142/s0218213006002576.