E 2.0 User Manual
Stephan Schulz · EasyChair preprint · 2018
E is an equational theorem prover for full first-order logic, based on superposition and rewriting. In this 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.