This is a short and currently very sketchy documentation to the E equational theorem prover. E is an purely equational theorem prover for first-order logic with equality. It is based on paramodulation and rewriting. This means that E reads a set of formulas and/or clauses and saturates it by systematically applying a number of inference rules until either all possible inferences have been performed or until the empty clause has been derived, i.e. the clause set has been found to be unsatisfiable and thus a conjecture has been proved.
E is still a moving target, but most recent releases have been quite stable, and the prover is being used productively by several independent groups of people. This manual should enable you to experiment with the prover and to use some of its more advanced features.
The manual assumes a working knowledge of refutational theorem proving, which can be gained from e.g. [CL73]. For a short description of E including performance data, see [Sch04]. A more detailed description has been published as [Sch02]. Most papers on E and much more information is available at or a few hops away from the E home page, http://www.eprover.org.
Some other provers have influenced the design of E and may be referenced in the course of this manual. These include SETHEO [MIL+97], Otter [McC94, MW97], SPASS [WGR96, WAB+99], DISCOUNT [DKS97], Waldmeister [HBF96, HJL99] and Vampire [RV02, RV01].