|
Abstract E is an equational theorem prover for full clausal logic, based on superposition and rewriting. In this very preliminary manual we first give a short introduction for impatient new users, and then cover calculus, control, options and input/output of the prover in some more detail. |