The E Equational Theorem Prover

E 0.999-006 Longview2 released! E 0.999-006 Longview2 is the latest release of our equational theorem prover. We believe it is one of the most powerful and friendly provers available for first-order logic today. You can get the source distribution below.

E is a a purely equational theorem prover for full first-order logic. That means it is a program that you can stuff a mathematical specification (in first-order format) and a hypothesis into, and which will then run forever, using up all of your machines resources. Very occasionally it will find a proof for the hypothesis and tell you so...

E's inference core is based on a modified version of the superposition calculus for equational clausal logic as described in [BG94]. For the case of pure unit equality (where both goals and axioms are simple equations, not disjunctions of literals or conditional rules), the calculus degenerates to unfailing completion [BDP89] extended to deal with arbitrarily quantified goals as implemented in DISCOUNT [DKS97]. Current versions offers a variety of literal selection functions and can e.g. emulate the unit-paramodulation strategy described in [Der91] for Horn clauses.

E can now also handle full first-order logic. It uses a standard clausification algorithm to translate first order formula to clausal logic. Both clausification and reasoning on the clausal form can be documented in checkable proof objects.

The prover was intended to become part of a METOP-based version of E-SETHEO [Mos96]. E-SETHEO now has evolved into a multi-paradigm strategy parallel proof system, but E is still a cornerstone of the system.

There is a short system description about E 0.999 on the CASC-21 website.

Documentation...

The default input language of E is a dialect of LOP developed for SETHEO. LOP is an extension of the PROLOG syntax, so people familiar with PROLOG should have little problems in reading LOP files.

E currently cannot handle constraints, and it will treat SETHEO build-in predicates as normal function symbols, which may result in strange and wondrous effects. E also demands that each symbol is used only as a function symbol, a predicate, or a constant (SETHEO allows the same symbol to take on more than one role in different contexts, which is clearly the Wrong Thing). That said, I have not yet encountered any difficulty in feeding SETHEO proof problems to E.

E interprets the special predicate equal() as the equality relation, and it will automatically translate non-equational literals into equational ones. Due to the special importance of this relation, it can also be represented by the infix symbols = (for equality) and != for inequality.

If you are like me, you can probably learn the syntax best from examples. There are a variety of them included with the distribution.

Newer versions of E can now also read (and write) classic TPTP format (versions 1 and 2) as well as the new TPTP-3/TSTP format.

Performance

Downloading

E is only available as a source distribution for various versions of UNIX. I have successfully compiled various versions of the prover out of the box under most UNIX versions I could lay hand on: Solaris 2.5, Solaris 2.6, Solaris 7, Solaris 8, Solaris 9, S.U.S.E. Linux 4.3, 5.2, 7.2 for Intel, Red Hat Linux 4.2 and 5.2 for SPARC, and, for the latest versions, MacOS-X 10.2.2-10.4.3. Successful compiles have also been achieved under SunOS 4.1.3, SunOS 4.1.4 (newer versions of E require some tweaking under old SunOS releases), FreeBSD, and HP-UX B 10.20 (see comments in Makefile.vars). I am pretty certain that the system will compile fine under most other current versions of GNU/Linux as well. You will need at least tar, gunzip, make, gcc (or another ANSI C compiler), and a reasonable version of ar to build the prover. These tools are usually already installed on or at least available for most UNIX-like systems. E has recently also been compiled succcessfully under Windows/Cygwin. The E distribution is free software and is available under the GNU GENERAL PUBLIC LICENSE (most official html version).

If you have any trouble, please tell me.

• Older versions are now available from a separate archive page.
• E 0.999-006 Longview2 (10-02-2008 - fixes minor TPTP-3 output bug)
  • The README file.
  • What's new compared to version 0.999.
  • The source distribution (~1350 kb)
  • Note that the latest users guide (PDF version) might be more complete than the version delivered with the distribution.

Additional Information and Links

Bibliography

[BDP89]

Bachmair, L.; Dershowitz, N.; Plaisted, D.A. (1989), Completion Without Failure, Resolution of Equations in Algebraic Structures, pp.1-30, Academic Press.

[BG94]

Bachmair, L.; Ganzinger, H. (1994), Rewrite-Based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation 4(3), pp.217-247.

[DKS97]

Denzinger, J.; Kronenburg, M.; Schulz, S. (1997), DISCOUNT: A Distributed and Learning Equational Prover, Journal of Automated Reasoning 18(2), pp.189-198.

[Der91]

Dershowitz, N. (1991), Ordering-Based Strategies for Horn Clauses, Proc. of the 12th IJCAI, Sydney, pp. 119-124, Morgan-Kaufmann

[Mos96]

Moser, M. (1996), Goal-Directed Resoning in Clausal Logic with Equality, PhD thesis, Institut für Informatik, Technische Universität München, Munich, Germany.

[Sch2000]

Schulz, S. (2000), Learning Search Control Knowledge for Equational Deduction, PhD Thesis, Akademische Verlagsgesellschaft Aka GmbH Berlin, 2000.

[Sch2002]

Schulz, S.(2002): E - A Brainiac Theorem Prover. Journal of AI Communications 15(2/3):111-126, 2002.

[Sch2004]

Schulz, S. (2004), System Abstract: E 0.81, Proc. 2nd IJCAR, Cork, Ireland, 2004, pp. 223-228, LNAI 3097, Springer.