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]
References
^Schulz, Stephan (2002). "E – A Brainiac Theorem Prover". Journal of AI Communications. 15 (2/3): 111–126.
^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.
ISBN978-3-540-42612-7.
^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.
ISBN978-3-540-71069-1. Archived from
the original(PDF) on 15 June 2011. Retrieved 20 December 2009.
^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.
ISBN978-3-540-71069-1.