The E Theorem Prover

 
 

E is a theorem prover for full first-order logic with equality. It accepts a problem specification, typically consisting of a number of first-order clauses or formulas, and a conjecture, again either in clausal or full first-order form. The system will then try to find a formal proof for the conjecture, assuming the axioms.


If a proof is found, the system can provide a detailed list of proof steps that can be individually verified. If the conjecture is existential (i.e. it’s of the form “there exists an X with property P”), the latest versions can also provide possible answers (values for X).


Development of E started as part of the E-SETHEO project at TUM. The first public release was in in 1998, and the system has been continuously improved ever since. I believe that E now is one of the most powerful and friendly reasoning systems for first-order logic. The prover has successfully participated in many competitions.

Overview

E 2.2 Thurbo Moonlight is available. It features a number of both user-visible and internal improvements, including:


  1. Direct integration of PicoSAT for propositional reasoning into a single stand-alone binary

  2. Improved automatic and strategy scheduling modes

  3. Check and enforce that  FOF, TCF and TFF are fully quantified, hopefully reducing user errors

  4. Detection and output of ContradictoryAxioms status in cases of an inconsistent specification

  5. Various minor improvements and bug-fixes


The new version is available from the Download page.

Latest news

E 2.3 Gielle is a new experimental version of E with optional support for lambda-free higher-order logic. It is based on E 2.2, and has, in general, the same features. If you are interested in higher-order features, please feel free to download and install this version and give us early feedback.


The new features have been developed in the context of the Matryoshka project, largely by Petar Vukmirovic, with input from several other project members.


E 2.3 (prerelease) is available from the Download page.