E equational theorem prover
Encyclopedia
E is a modern, high performance theorem prover
for full first-order logic
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 was developed by Stephan Schulz, originally in the Automated Reasoning Group at TU Munich
.
. 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.
E is implemented in C
and portable to most UNIX
dialects and the Cygwin
environment.
It is available under the GNU GPL
.
, 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 of E include reasoning on large ontologies, software verification, and software certification.
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
for full first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
with equality. It is based on the equational superposition calculus
Superposition calculus
The superposition calculus is a calculus for reasoning in equational first-order logic. It has been developed in the early 1990s and combines concepts from first-order resolution with ordering-based equality handling as developed in the context of Knuth-Bendix completion...
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 was developed by Stephan Schulz, originally in the Automated Reasoning Group at TU Munich
Technical University of Munich
The Technische Universität München is a research university with campuses in Munich, Garching, and Weihenstephan...
.
System
The system is based on the equational superposition calculusSuperposition calculus
The superposition calculus is a calculus for reasoning in equational first-order logic. It has been developed in the early 1990s and combines concepts from first-order resolution with ordering-based equality handling as developed in the context of Knuth-Bendix completion...
. 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
Term indexing
In computer science, term indexing is the task of creating an index of terms and clauses in a collection.Many operations in automatic theorem provers require search in hugecollections of terms and clauses. Such operations typically fall into...
data structures for speeding up inferences, advanced inference literal selection strategies, and various uses of machine learning techniques to improve the search behaviour.
E is implemented in C
C (programming language)
C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....
and portable to most UNIX
Unix
Unix is a multitasking, multi-user computer operating system originally developed in 1969 by a group of AT&T employees at Bell Labs, including Ken Thompson, Dennis Ritchie, Brian Kernighan, Douglas McIlroy, and Joe Ossanna...
dialects and the Cygwin
Cygwin
Cygwin is a Unix-like environment and command-line interface for Microsoft Windows. Cygwin provides native integration of Windows-based applications, data, and other system resources with applications, software tools, and data of the Unix-like environment...
environment.
It is available under the GNU GPL
GNU General Public License
The GNU General Public License is the most widely used free software license, originally written by Richard Stallman for the GNU Project....
.
Competitions
The prover has consistently performed well in the CADE ATP System CompetitionCADE ATP System Competition
The CADE ATP System Competition is a yearly competition of fully automated theorem provers for classical first order logic. CASC is associated with the Conference on Automated Deduction and the International Joint Conference on Automated Reasoning organized by the Association for Automated...
, 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 and SPASS, 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.