E (theorem prover)

E is a high-performance theorem prover for full first-order logic with equality. 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 the Technical University of 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), 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. Since version 2.0, E supports many-sorted logic.

E is implemented in C and portable to most UNIX variants and the Cygwin environment. It is available under the GNU GPL.

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. In 2008 it came in second place. 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). It repeated the performance in FOF and CNF in 2010, and won a special award as "overall best" system. In the 2011 CASC-23 E won the CNF division and achieved second places in UEQ and LTB.

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. E also is the reasoning engine in SInE and LEO-II and used as the clausification system for iProver.

Applications of E include reasoning on large ontologies, software verification, and software certification.

References

  1. ↑ Schulz, Stephan (2002). "E – A Brainiac Theorem Prover". Journal of AI Communications. 15 (2/3): 111–126.
  2. 1 2 Schulz, Stephan (2008). "Entrants System Descriptions: E 1.0pre and EP 1.0pre". Archived from the original on 15 June 2009. Retrieved 24 March 2009.
  3. ↑ Schulz, Stephan (2004). "System Description: E 0.81". Automated Reasoning. Lecture Notes in Computer Science. Vol. 3097. pp. 223–228. doi:10.1007/978-3-540-25984-8_15. ISBN 978-3-540-22345-0.
  4. ↑ Schulz, Stephan (2001). "Learning Search Control Knowledge for Equational Theorem Proving". KI 2001: Advances in Artificial Intelligence. Lecture Notes in Computer Science. Vol. 2174. pp. 320–334. doi:10.1007/3-540-45422-5_23. ISBN 978-3-540-42612-7.
  5. ↑ "news on E's website". Retrieved 10 July 2017.
  6. ↑ Schulz, Stephan (2008). "The E Equational Theorem Prover". Retrieved 24 March 2009.
  7. ↑ Sutcliffe, Geoff. "The CADE ATP System Competition". Archived from the original on 2 March 2009. Retrieved 24 March 2009.
  8. ↑ "FOF division of CASC in 2008". Archived from the original on 15 June 2009. Retrieved 19 December 2009.
  9. ↑ Sutcliffe, Geoff (2009). "The 4th IJCAR Automated Theorem Proving System Competition--CASC-J4". AI Communications. 22 (1): 59–72. doi:10.3233/AIC-2009-0441.
  10. ↑ Sutcliffe, Geoff (2010). "The CADE ATP System Competition". University of Miami. Archived from the original on 29 June 2010. Retrieved 20 July 2010.
  11. ↑ Sutcliffe, Geoff (2011). "The CADE ATP System Competition". University of Miami. Archived from the original on 12 August 2011. Retrieved 14 August 2011.
  12. ↑ 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.
  13. ↑ Meng, Jia; Lawrence C. Paulson (2004). Experiments on Supporting Interactive Proof Using Resolution. Lecture Notes in Computer Science. Vol. 3097. Springer. pp. 372–384. doi:10.1007/978-3-540-25984-8_28. ISBN 978-3-540-22345-0.
  14. ↑ Sutcliffe, Geoff; et al. (2009). The 4th IJCAR ATP System Competition (PDF). Archived from the original (PDF) on 17 June 2009. Retrieved 18 December 2009.
  15. ↑ 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)". Automated Reasoning (PDF). Lecture Notes in Computer Science. Vol. 5195. Springer. pp. 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.
  16. ↑ Korovin, Konstantin (2008). "iProver—an instantiation-based theorem prover for first-order logic". Automated Reasoning. Lecture Notes in Computer Science. Vol. 5195. pp. 292–298. doi:10.1007/978-3-540-71070-7_24. ISBN 978-3-540-71069-1.
  17. ↑ 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.
  18. ↑ Ranise, Silvio; David Déharbe (2003). "Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs". Electronic Notes in Theoretical Computer Science. 86 (1). 4th International Workshop on First-Order Theorem Proving: Elsevier: 109–119. doi:10.1016/S1571-0661(04)80656-X.{{cite journal}}: CS1 maint: location (link)
  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. doi:10.1142/s0218213006002576. Archived from the original on 24 February 2012. Retrieved 19 December 2009.