# E equational theorem prover

### From Seo Wiki - Search Engine Optimization and Programming Languages

**E** is a modern, high performance theorem prover for full first-order logic with equality.^{[1]} It's 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 has been developed by Stephan Schulz, originally in the *Automated Reasoning Group* at TU Munich.

## Contents |

## 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.^{[3]}^{[2]}^{[4]}

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

## 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.^{[6]} In 2008 it came in second place.^{[7]} 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).^{[8]}

## Applications

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

Applications of E include reasoning on large ontologies^{[14]}, software verification,^{[15]} and software certification.^{[16]}

## Author

Stephan Schulz is a German computer scientist working in the field of automated reasoning. In 2002, Schulz was recognized by the Florida Artificial Intelligence Research Society with the *best paper* award for his work *A Comparison of Different Techniques for Grounding Near-Propositional CNF Formulae*. ^{[17]} Together with Geoff Sutcliffe, Schulz founded and has been organizing the ES* Workshop series, a venue for presentation and publishing of practically oriented Automated Reasoning research.^{[18]} He has been significantly involved with the IWIL Workshop series on implementations of logics, and is a member of the Steering Committee of the International Workshop on First-Order Theorem Proving.^{[19]}

## References

- ↑ Schulz, Stephan (2002). "E - A Brainiac Theorem Prover".
*Journal of AI Communications***15**(2/3): 111–126. - ↑
^{2.0}^{2.1}Schulz, Stephan (2008). "Entrants System Descriptions: E 1.0pre and EP 1.0pre". http://www.cs.miami.edu/~tptp/CASC/J4/SystemDescriptions.html#E---1.0pre. Retrieved 2009-03-24. - ↑ Schulz, Stephan (2004). "System Description: E 0.81".
*Proceedings of the 2nd International Joint Conference on Automated Reasoning*(Springer)**LNAI 3097**: 223–228. - ↑ Schulz, Stephan (2001). "Learning Search Control Knowledge for Equational Theorem Proving".
*Proceedings of the Joint German/Austrian Conference on Artificial Intelligence (KI-2001)*(Springer)**LNAI 2174**: 320–334. - ↑ Schulz, Stephan (2008). "The E Equational Theorem Prover". http://www.eprover.org. Retrieved 2009-03-24.
- ↑ Sutcliffe, Geoff. "The CADE ATP System Competition". http://www.cs.miami.edu/~tptp/CASC/. Retrieved 2009-03-24.
- ↑ 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. http://iospress.metapress.com/content/f94jp575q0h146v7/. Retrieved 2009-12-16. - ↑ Paulson, Lawrence C. (2008). "Automation for Interactive Proof: Techniques, Lessons and Prospects".
*Tools and Techniques for Verification of System Infrastructure - A Festschrift in Honour of Professor Michael J. C. Gordon FRS*: 29–30. http://ttvsi.gilith.com/ttvsi.pdf#page=39. Retrieved 2009-12-19. - ↑ Meng, Jia; Lawrence C. Paulson (2004). "Experiments on Supporting Interactive Proof Using Resolution".
*LNCS*(Springer)**3097**: 372-384}. http://www.springerlink.com/content/btx6b2rrewvmjc9y/. Retrieved 2009-12-16. - ↑ Sutcliffe, Geoff; et al (2009).
*The 4th IJCAR ATP System Competition*. http://www.cs.miami.edu/~tptp/CASC/J4/Proceedings.pdf. Retrieved 2009-12-18. - ↑ Benzmüller, Christoph; Lawrence C. Paulson, Frank Theiss , and Arnaud Fietzke (2008). "LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)".
*LNCS*(4th International Joint Conference on Automated Reasoning, IJCAR 2008 Sydney, Australia: Springer)**5195**: 162–170. http://www.ags.uni-sb.de/~chris/papers/C26.pdf. - ↑ Korovin, Konstantin (2008). "iProver—an instantiation-based theorem prover for first-order logic (system description)".
*LNCS*(Springer)**5195**: 292–298. http://www.cs.manchester.ac.uk/~korovink/my_pub/iprover_descr_08.pdf. Retrieved 2009-12-18. - ↑ Ramachandran, Deepak; Pace Reagan and Keith Goolsbery (2005). "First-Orderized ResearchCyc : Expressivity and Efficiency in a Common-Sense Ontology".
*AAAI Workshop on Contexts and Ontologies: Theory, Practice and Applications*(AAAI). https://www.aaai.org/Papers/Workshops/2005/WS-05-01/WS05-01-006.pdf. - ↑ 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. http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75H1-4DDWKNY-ND&_user=10&_rdoc=1&_fmt=&_orig=search&_sort=d&_docanchor=&view=c&_rerunOrigin=scholar.google&_acct=C000050221&_version=1&_urlVersion=0&_userid=10&md5=7c3d4c7c9b56361f82b30edf963c5443. Retrieved 2009-18-12. - ↑ Denney, Ewen; Bernd Fischer and Johan Schumann (2006). "An Empirical Evaluation of Automated Theorem Provers in Software Certification".
*International Journal on Artificial Intelligence Tools***15**(1): 81–107. http://eprints.ecs.soton.ac.uk/12355/. - ↑ "Flairs 2002 Conference Report".
*AI Magazine*. 2002-12. http://www.accessmylibrary.com/coms2/summary_0286-27024342_ITM. - ↑ Schulz, Stephan. "Empirically Successful Topics in Automated Deduction". http://www.eprover.org/EVENTS/es_series.html. Retrieved 19 December 2009.
- ↑ "Home page of FTP workshops/Steering Committee". http://www.csc.liv.ac.uk/FTP-WS/index.html#committee. Retrieved 19 December 2009.