E is a high-performance theorem prover for full

first-order logic First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...

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 TU Munich, now at

Baden-Württemberg Cooperative State University The Baden-Württemberg Cooperative State University (German: ''Duale Hochschule Baden-Württemberg'', DHBW) is an institution of higher education with several campuses throughout the state of Baden-Württemberg, Germany. It offers dual-educati ...

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 Many-sorted logic can reflect formally our intention not to handle the universe as a homogeneous collection of objects, but to partition it in a way that is similar to types in typeful programming. Both functional and assertive " parts of speech ...

. E is implemented in C and portable to most

UNIX Unix (, ; trademarked as UNIX) is a family of multitasking, multi-user computer operating systems that derive from the original AT&T Unix, whose development started in 1969 at the Bell Labs research center by Ken Thompson, Dennis Ritchie, a ...

variants and the

Cygwin Cygwin ( ) is a free and open-source Unix-like environment and command-line interface (CLI) for Microsoft Windows. The project also provides a software repository containing open-source packages. Cygwin allows source code for Unix-like operati ...

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 A vampire is a mythical creature that subsists by feeding on the Vitalism, vital essence (generally in the form of blood) of the living. In European folklore, vampires are undead, undead humanoid creatures that often visited loved ones and c ...

) 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

, 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

External links

E home page
{{DEFAULTSORT:E Theorem Prover Free software programmed in C Free theorem provers Unix programming tools Software using the GNU General Public License