Download E 1.7 User Manual - Software and Systems Engineering

Abstract
E is an equational theorem prover for full first-order logic, based on superposition and rewriting. In this perpetually very preliminary manual we first give a
short introduction for impatient new users, and then cover calculus and proof
procedure. The manual covers proof search control and related options, followed
by input and output formats. Finally, it describes some additional tools that
are part of the E distribution.