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 quantifie ...

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 (unfa ...

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. Establis ...

, 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 clauses in a logic program, deductive database, or automated theorem prover. Overview Many operations in automatic theorem provers require search in hu ...

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" i ...

. E is implemented in C and portable to most

UNIX Unix (; trademarked as UNIX) is a family of multitasking, multiuser 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, and ot ...

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 in ...

environment. It is available under the

GNU GPL The GNU General Public License (GNU GPL or simply GPL) is a series of widely used free software licenses that guarantee end users the four freedoms to run, study, share, and modify the software. The license was the first copyleft for general us ...

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 organi ...

, 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 creatures that often visited loved ones and caused mi ...

) 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 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 wit ...

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 popul ...

'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