Stephan Schulz: E -- A Brainiac Theorem Prover  

Abstract:

We describe the superposition-based theorem prover E. E is a sound and
complete prover for clausal first order logic with equality.
Important properties of the prover include strong redundancy
elimination criteria, the DISCOUNT loop proof procedure, a very
flexible interface for specifying search control heuristics, and an
efficient inference engine. We also discuss strength and weaknesses of
the system.