E (theorem prover)
Template:Use dmy dates E is a high-performance theorem prover for full first-order logic with equality.<ref name=brainiac>Template:Cite journal</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 TU Munich, now at Baden-Württemberg Cooperative State University Stuttgart.
SystemEdit
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>{{#invoke:citation/CS1|citation |CitationClass=web }}</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>Template:Cite book</ref><ref>Template:Cite book</ref> Since version 2.0, E supports many-sorted logic.<ref>{{#invoke:citation/CS1|citation |CitationClass=web }}</ref>
E is implemented in C and portable to most UNIX variants and the Cygwin environment. It is available under the GNU GPL.<ref>{{#invoke:citation/CS1|citation |CitationClass=web }}</ref>
CompetitionsEdit
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>{{#invoke:citation/CS1|citation |CitationClass=web }}</ref> In 2008 it came in second place.<ref>{{#invoke:citation/CS1|citation |CitationClass=web }}</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) in CNF (clausal logic).<ref name="casc2009">Template:Cite journal</ref> It repeated the performance in FOF and CNF in 2010, and won a special award as "overall best" system.<ref>{{#invoke:citation/CS1|citation |CitationClass=web }}</ref> In the 2011 CASC-23 E won the CNF division and achieved second places in UEQ and LTB.<ref>{{#invoke:citation/CS1|citation |CitationClass=web }}</ref>
ApplicationsEdit
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.<ref>Template:Cite journal</ref><ref>Template:Cite book</ref> E also is the reasoning engine in SInE<ref>Template:Cite book</ref> and LEO-II<ref>Template:Cite book</ref> and used as the clausification system for iProver.<ref>Template:Cite book</ref>
Applications of E include reasoning on large ontologies,<ref>Template:Cite journal</ref> software verification,<ref>Template:Cite journal</ref> and software certification.<ref>Template:Cite journal</ref>