Editing E (theorem prover) (section)

==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>