Editing E (theorem prover)

{{Use dmy dates|date=March 2024}}
'''E''' is a high-performance [[Automated theorem proving|theorem prover]] for full [[first-order logic]] with equality.<ref name=brainiac>{{Cite journal
| first=Stephan
| last=Schulz
| title=E – A Brainiac Theorem Prover
| journal=Journal of AI Communications
| volume=15
| issue=2/3
| pages=111–126
| year=2002
}}</ref> 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 [[Technical University of Munich|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),<ref name=casc2008>{{Cite web|url=http://www.cs.miami.edu/~tptp/CASC/J4/SystemDescriptions.html#E---1.0pre|title=Entrants System Descriptions: E 1.0pre and EP 1.0pre|last=Schulz|first=Stephan|year=2008|accessdate=2009-03-24|archive-date=15 June 2009|archive-url=https://web.archive.org/web/20090615180620/http://www.cs.miami.edu/~tptp/CASC/J4/SystemDescriptions.html#E---1.0pre|url-status=dead}}</ref> 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.<ref name=casc2008/><ref>{{Cite book|last=Schulz|first=Stephan|title=Automated Reasoning |chapter=System Description: E 0.81 |year=2004 |pages=223–228|doi=10.1007/978-3-540-25984-8_15|series=Lecture Notes in Computer Science|volume=3097 |isbn=978-3-540-22345-0}}</ref><ref>{{Cite book|last=Schulz|first=Stephan|title=KI 2001: Advances in Artificial Intelligence |chapter=Learning Search Control Knowledge for Equational Theorem Proving |year=2001 |pages=320–334|doi=10.1007/3-540-45422-5_23|series=Lecture Notes in Computer Science|volume=2174 |isbn=978-3-540-42612-7}}</ref> Since version 2.0, E supports [[many-sorted logic]].<ref>{{Cite web|url=https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html|accessdate=2017-07-10|title=news on E's website}}</ref>

E is implemented in [[C (programming language)|C]] and portable to most [[Unix|UNIX]] variants and the [[Cygwin]] environment. It is available under the [[GNU General Public License|GNU GPL]].<ref>{{Cite web|url=http://www.eprover.org|title=The E Equational Theorem Prover|last=Schulz|first=Stephan|year=2008|accessdate=2009-03-24}}</ref>

==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.<ref>{{Cite web|url=http://www.cs.miami.edu/~tptp/CASC/|title=The CADE ATP System Competition|last=Sutcliffe|first=Geoff|accessdate=2009-03-24|archive-url=https://web.archive.org/web/20090302112038/http://www.cs.miami.edu/~tptp/CASC/|archive-date=2 March 2009|url-status=dead}}</ref> In 2008 it came in second place.<ref>{{Cite web |url=http://www.cs.miami.edu/~tptp/CASC/J4/WWWFiles/DivisionSummary.html |title=FOF division of CASC in 2008 |access-date=19 December 2009 |archive-date=15 June 2009 |archive-url=https://web.archive.org/web/20090615151700/http://www.cs.miami.edu/~tptp/CASC/J4/WWWFiles/DivisionSummary.html |url-status=dead }}</ref> 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 (theorem prover)|Vampire]]) in [[Conjunctive normal form|CNF]] (clausal logic).<ref name="casc2009">{{Cite journal|last=Sutcliffe|first=Geoff|year=2009|title=The 4th IJCAR Automated Theorem Proving System Competition--CASC-J4|journal=AI Communications|volume=22|issue=1|pages=59–72|url=http://iospress.metapress.com/content/f94jp575q0h146v7/|accessdate=2009-12-16|doi=10.3233/AIC-2009-0441|url-access=subscription}}</ref> It repeated the performance in FOF and CNF in 2010, and won a special award as "overall best" system.<ref>{{Cite web|last=Sutcliffe|first=Geoff|title=The CADE ATP System Competition|url=http://www.cs.miami.edu/~tptp/CASC/J5/|publisher=University of Miami|accessdate=20 July 2010|year=2010|archive-date=29 June 2010|archive-url=https://web.archive.org/web/20100629053023/http://www.cs.miami.edu/~tptp/CASC/J5/|url-status=dead}}</ref> In the 2011 CASC-23 E won the CNF division and achieved second places in UEQ and LTB.<ref>{{Cite web|last=Sutcliffe|first=Geoff|title=The CADE ATP System Competition|url=http://www.cs.miami.edu/~tptp/CASC/23/|publisher=University of Miami|accessdate=14 August 2011|year=2011|archive-date=12 August 2011|archive-url=https://web.archive.org/web/20110812082814/http://www.cs.miami.edu/~tptp/CASC/23/|url-status=dead}}</ref>

==Applications==
E has been integrated into several other theorem provers. It is, with [[Vampire (theorem prover)|Vampire]], [[SPASS]], [http://cvc4.cs.stanford.edu/web/ CVC4], and [[Z3 Theorem Prover|Z3]], at the core of [[Isabelle (theorem prover)|Isabelle]]'s ''Sledgehammer'' strategy.<ref>{{Cite journal|last=Paulson  |first=Lawrence C. |year=2008|title=Automation for Interactive Proof: Techniques, Lessons and Prospects|journal=Tools and Techniques for Verification of System Infrastructure – A Festschrift in Honour of Professor Michael J. C. Gordon FRS|pages=29–30|url=http://ttvsi.gilith.com/ttvsi.pdf#page=39|accessdate=2009-12-19}}</ref><ref>{{Cite book|last=Meng|first=Jia|author2=Lawrence C. Paulson|date=2004|title=Experiments on Supporting Interactive Proof Using Resolution |publisher=Springer|volume=3097|pages=372–384|doi=10.1007/978-3-540-25984-8_28|series=Lecture Notes in Computer Science|isbn=978-3-540-22345-0|citeseerx=10.1.1.62.5009}}</ref> E also is the reasoning engine in SInE<ref>{{Cite book|last=Sutcliffe|first=Geoff|title=The 4th IJCAR ATP System Competition|year=2009|url=http://www.cs.miami.edu/~tptp/CASC/J4/Proceedings.pdf|accessdate=2009-12-18|display-authors=etal|archive-date=17 June 2009|archive-url=https://web.archive.org/web/20090617103841/http://www.cs.miami.edu/~tptp/CASC/J4/Proceedings.pdf|url-status=dead}}</ref> and LEO-II<ref>{{Cite book|last=Benzmüller|first=Christoph|author2=Lawrence C. Paulson|author3=Frank Theiss|author4=Arnaud Fietzke|title=Automated Reasoning |chapter=LEO-II – A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) |year=2008|publisher=Springer|volume=5195|pages=162–170|url=http://www.ags.uni-sb.de/~chris/papers/C26.pdf|doi=10.1007/978-3-540-71070-7_14|series=Lecture Notes in Computer Science|isbn=978-3-540-71069-1|access-date=20 December 2009|archive-url=https://web.archive.org/web/20110615131639/http://www.ags.uni-sb.de/~chris/papers/C26.pdf|archive-date=15 June 2011|url-status=dead}}</ref> and used as the clausification system for iProver.<ref>{{Cite book|last=Korovin|first=Konstantin|year=2008|title= Automated Reasoning|chapter=iProver—an instantiation-based theorem prover for first-order logic |doi=10.1007/978-3-540-71070-7_24|series=Lecture Notes in Computer Science|volume=5195|pages=292–298|isbn=978-3-540-71069-1}}</ref>

Applications of E include reasoning on large ontologies,<ref>{{Cite journal|last=Ramachandran|first=Deepak |author2=Pace Reagan |author3=Keith Goolsbery|year=2005|title=First-Orderized ResearchCyc : Expressivity and Efficiency in a Common-Sense Ontology|journal=AAAI Workshop on Contexts and Ontologies: Theory, Practice and Applications|publisher=AAAI|url=https://www.aaai.org/Papers/Workshops/2005/WS-05-01/WS05-01-006.pdf}}</ref> software verification,<ref>{{Cite journal|last=Ranise|first=Silvio|author2=David Déharbe|year=2003|title=Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs|journal=Electronic Notes in Theoretical Computer Science|publisher=Elsevier|location=4th International Workshop on First-Order Theorem Proving|volume=86|issue=1|pages=109–119|doi=10.1016/S1571-0661(04)80656-X|doi-access=free}}</ref> and software certification.<ref>{{Cite journal|last=Denney|first=Ewen|author2=Bernd Fischer|author3=Johan Schumann|year=2006|title=An Empirical Evaluation of Automated Theorem Provers in Software Certification|journal=International Journal on Artificial Intelligence Tools|volume=15|issue=1|pages=81–107|url=http://eprints.ecs.soton.ac.uk/12355/|doi=10.1142/s0218213006002576|citeseerx=10.1.1.163.4861|access-date=19 December 2009|archive-date=24 February 2012|archive-url=https://web.archive.org/web/20120224182009/http://eprints.ecs.soton.ac.uk/12355/|url-status=dead}}</ref>

==References==
{{Reflist}}

==External links==
*[https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html E home page]
*[https://wwwlehre.dhbw-stuttgart.de/~sschulz/DHBW_Stephan_Schulz/Stephan_Schulz.html E's developer]

{{DEFAULTSORT:E Theorem Prover}}
[[Category:Free software programmed in C]]
[[Category:Free theorem provers]]
[[Category:Unix programming tools]]
[[Category:Software using the GNU General Public License]]