E is a high-performance theorem prover for full

first-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifi ...

with equality. It is based on the equational

superposition calculus The superposition calculus is a calculus for reasoning in equational first-order logic. It was developed in the early 1990s and combines concepts from first-order resolution with ordering-based equality handling as developed in the context of (unf ...

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 The Technical University of Munich (TUM or TU Munich; german: Technische Universität München) is a public research university in Munich, Germany. It specializes in engineering, technology, medicine, and applied and natural sciences. Establ ...

, 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-educat ...

Stuttgart.

System

The system is based on the equational

. 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 In computer science, a term index is a data structure to facilitate fast lookup of terms and Clause (logic), clauses in a logic programming, logic program, deductive database, or automated theorem prover. Overview Many operations in automatic the ...

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 variants and the

Cygwin Cygwin ( ) is a POSIX-compatible programming and runtime environment that runs natively on Microsoft Windows. Under Cygwin, source code designed for Unix-like operating systems may be compiled with minimal modification and executed. The Cygwin i ...

environment. It is available under the GNU GPL.

Competitions

The prover has consistently performed well in the

CADE ATP System Competition The CADE ATP System Competition (CASC) is a yearly competition of fully automated theorem provers for classical logic CASC is associated with the Conference on Automated Deduction and the International Joint Conference on Automated Reasoning orga ...

, 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 SPASS is an automated theorem prover for first-order logic with equality developed at the Max Planck Institute for Computer Science and using the superposition calculus. The name originally stood for ''Synergetic Prover Augmenting Superposition wi ...

CVC4
an
Z3
at the core of

Isabelle Isabel is a female name of Spanish origin. Isabelle is a name that is similar, but it is of French origin. It originates as the medieval Spanish form of '' Elisabeth'' (ultimately Hebrew '' Elisheva''), Arising in the 12th century, it became popu ...

'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