Stephan Schulz: "System Abstract: E 0.61"

Abstract:

We describe the main characteristics of version 0.61 of the E
equational theorem prover. E is based on superposition (with literal
selection) and rewriting.  A particular strength of E is the ability
to control the proof search very well. This is reflected by a very
powerful and flexible interface for the specification of clause
selection functions, and by a wide variety of functions for the
selection of inference literals.  We discuss some important aspects of
the implementation and demonstrate the performance of the prover by
presenting experimental results on the TPTP. Finally, we describe our
future plans for the system.