E (theorem prover) explained

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]

External links

Notes and References

  1. Stephan. Schulz. E – A Brainiac Theorem Prover. Journal of AI Communications. 15. 2/3. 111–126. 2002.
  2. Web site: Entrants System Descriptions: E 1.0pre and EP 1.0pre. Schulz. Stephan. 2008. 2009-03-24. 15 June 2009. https://web.archive.org/web/20090615180620/http://www.cs.miami.edu/~tptp/CASC/J4/SystemDescriptions.html#E---1.0pre. dead.
  3. Book: Schulz, Stephan. Automated Reasoning . System Description: E 0.81 . 2004 . 223–228. 10.1007/978-3-540-25984-8_15. Lecture Notes in Computer Science. 3097 . 978-3-540-22345-0.
  4. Book: Schulz, Stephan. KI 2001: Advances in Artificial Intelligence . Learning Search Control Knowledge for Equational Theorem Proving . 2001 . 320–334. 10.1007/3-540-45422-5_23. Lecture Notes in Computer Science. 2174 . 978-3-540-42612-7.
  5. Web site: news on E's website. 2017-07-10.
  6. Web site: The E Equational Theorem Prover. Schulz. Stephan. 2008. 2009-03-24.
  7. Web site: The CADE ATP System Competition. Sutcliffe. Geoff. 2009-03-24. https://web.archive.org/web/20090302112038/http://www.cs.miami.edu/~tptp/CASC/. 2 March 2009. dead.
  8. Web site: FOF division of CASC in 2008 . 19 December 2009 . 15 June 2009 . https://web.archive.org/web/20090615151700/http://www.cs.miami.edu/~tptp/CASC/J4/WWWFiles/DivisionSummary.html . dead .
  9. Sutcliffe. Geoff. 2009. The 4th IJCAR Automated Theorem Proving System Competition--CASC-J4. AI Communications. 22. 1. 59–72. 2009-12-16. 10.3233/AIC-2009-0441.
  10. Web site: Sutcliffe. Geoff. The CADE ATP System Competition. University of Miami. 20 July 2010. 2010. 29 June 2010. https://web.archive.org/web/20100629053023/http://www.cs.miami.edu/~tptp/CASC/J5/. dead.
  11. Web site: Sutcliffe. Geoff. The CADE ATP System Competition. University of Miami. 14 August 2011. 2011. 12 August 2011. https://web.archive.org/web/20110812082814/http://www.cs.miami.edu/~tptp/CASC/23/. dead.
  12. 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. 2009-12-19.
  13. Book: Meng, Jia. Lawrence C. Paulson. 2004. Experiments on Supporting Interactive Proof Using Resolution . Springer. 3097. 372–384. 10.1007/978-3-540-25984-8_28. Lecture Notes in Computer Science. 978-3-540-22345-0. 10.1.1.62.5009.
  14. Book: Sutcliffe, Geoff. The 4th IJCAR ATP System Competition. 2009. 2009-12-18. etal. 17 June 2009. https://web.archive.org/web/20090617103841/http://www.cs.miami.edu/~tptp/CASC/J4/Proceedings.pdf. dead.
  15. Book: Benzmüller, Christoph. Lawrence C. Paulson. Frank Theiss. Arnaud Fietzke. Automated Reasoning . LEO-II – A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) . 2008. Springer. 5195. 162–170. 10.1007/978-3-540-71070-7_14. Lecture Notes in Computer Science. 978-3-540-71069-1. 20 December 2009. https://web.archive.org/web/20110615131639/http://www.ags.uni-sb.de/~chris/papers/C26.pdf. 15 June 2011. dead.
  16. Book: Korovin, Konstantin. 2008. Automated Reasoning. iProver—an instantiation-based theorem prover for first-order logic . 10.1007/978-3-540-71070-7_24. Lecture Notes in Computer Science. 5195. 292–298. 978-3-540-71069-1.
  17. Ramachandran. Deepak . Pace Reagan . 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.
  18. Ranise. Silvio. David Déharbe. 2003. Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs. Electronic Notes in Theoretical Computer Science. Elsevier. 4th International Workshop on First-Order Theorem Proving. 86. 1. 109–119. 10.1016/S1571-0661(04)80656-X. free.
  19. 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. 10.1142/s0218213006002576. 10.1.1.163.4861. 19 December 2009. 24 February 2012. https://web.archive.org/web/20120224182009/http://eprints.ecs.soton.ac.uk/12355/. dead.

This article is licensed under the GNU Free Documentation License. It uses material from the Wikipedia article "E (theorem prover)".

Except where otherwise indicated, Everything.Explained.Today is © Copyright 2009-2024, A B Cryer, All Rights Reserved. Cookie policy.