×

E – a brainiac theorem prover. (English) Zbl 1020.68084

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.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite