Schulz, Stephan E – a brainiac theorem prover. (English) Zbl 1020.68084 AI Commun. 15, No. 2-3, 111-126 (2002). Summary: 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. Cited in 89 Documents MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:superposition-based theorem prover Software:E Theorem Prover PDFBibTeX XMLCite \textit{S. Schulz}, AI Commun. 15, No. 2--3, 111--126 (2002; Zbl 1020.68084)