![[ It's Rational! ]](http://www.saintaardvarkthecarpeted.com/images/ayn_seal_of_approval_button.jpg)
E 1.2 Badamtam released! E 1.2 Badamtam is the latest release of the first-order theorem prover E. This version participated in CASC-J5 and won second place in the FOF (full first order) division and was highly placed in CNF and UEQ. I also won the special "best prover overall" award. We believe it is one of the most powerful and friendly provers available for first-order logic today. E is available as a free download under the terms of the GNU GPL or GNU LGPL 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 handle full first-order logic. It uses an efficiently implemented version of the clausification algorithm described in [NW2001] 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 originally intended to become part of a METOP-based version of E-SETHEO [Mos96]. E-SETHEO has evolved into a multi-paradigm strategy parallel proof system. E is still a cornerstone of the latest release of the system, but it also has taken on a life of its own.
There is a short system description of E 1.2 on the CASC-J5 website.
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.
E is 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. See below for a link to pre-build Windows binaries. 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.