E (theorem prover)

Quality 0.50 · 4 views · Updated 2 months ago

title: "E (theorem prover)" type: doc version: 1 created: 2026-02-28 author: "Wikipedia contributors" status: active scope: public tags: ["free-software-programmed-in-c", "free-theorem-provers", "unix-programming-tools", "software-using-the-gnu-general-public-license"] topic_path: "technology/operating-systems" source: "https://en.wikipedia.org/wiki/E_(theorem_prover)" license: "CC BY-SA 4.0" wikipedia_page_id: 0 wikipedia_revision_id: 0

E is a high-performance theorem prover for full first-order logic with equality.{{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

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 .

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

References

References

  1. Schulz, Stephan. (2008). "Entrants System Descriptions: E 1.0pre and EP 1.0pre".
  2. Schulz, Stephan. (2004). "Automated Reasoning".
  3. Schulz, Stephan. (2001). "KI 2001: Advances in Artificial Intelligence".
  4. "news on E's website".
  5. Schulz, Stephan. (2008). "The E Equational Theorem Prover".
  6. Sutcliffe, Geoff. "The CADE ATP System Competition".
  7. "FOF division of CASC in 2008".
  8. Sutcliffe, Geoff. (2009). "The 4th IJCAR Automated Theorem Proving System Competition--CASC-J4". AI Communications.
  9. Sutcliffe, Geoff. (2010). "The CADE ATP System Competition". University of Miami.
  10. Sutcliffe, Geoff. (2011). "The CADE ATP System Competition". University of Miami.
  11. 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.
  12. Meng, Jia. (2004). "Experiments on Supporting Interactive Proof Using Resolution". Springer.
  13. Sutcliffe, Geoff. (2009). "The 4th IJCAR ATP System Competition".
  14. Benzmüller, Christoph. (2008). "Automated Reasoning". Springer.
  15. Korovin, Konstantin. (2008). "Automated Reasoning".
  16. Ramachandran, Deepak. (2005). "First-Orderized ResearchCyc : Expressivity and Efficiency in a Common-Sense Ontology". AAAI.
  17. Ranise, Silvio. (2003). "Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs". Elsevier.
  18. Denney, Ewen. (2006). "An Empirical Evaluation of Automated Theorem Provers in Software Certification". International Journal on Artificial Intelligence Tools.

::callout[type=info title="Wikipedia Source"] This article was imported from Wikipedia and is available under the Creative Commons Attribution-ShareAlike 4.0 License. Content has been adapted to SurfDoc format. Original contributors can be found on the article history page. ::

free-software-programmed-in-cfree-theorem-proversunix-programming-toolssoftware-using-the-gnu-general-public-license