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.


E 1.9.1 Sungma is available. It features a number of improvements, including:

  1. Improved automatic and strategy scheduling modes

  2. Much Improved support for using the watchlist to provide hints

  3. Automatic detection of input format and selection of suitable output format

  4. Various minor improvements and bug-fixes, including a nasty if rarely triggered bug in clausification

The new version is available from the Download page.

Latest news