Stephan Schulz: "System Abstract: E 0.3"

Abstract:

We describe the main characteristics of version 0.3 of the E
equational theorem prover. E is based on superposition and
rewriting. It features a powerful interface for specifying search
guiding heuristics. We discuss some important details of the
implementation and demonstrate the performance of the prover by
presenting experimental results on the TPTP. Finally, we describe
our future plans for improving the system.