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 (un ...
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-educat ...
Stuttgart.
System
The system 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 (un ...
. 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 ...
.
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, 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 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 ...
, 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'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