zbMATH — the first resource for mathematics

System description: E 1.8. (English) Zbl 1407.68442
McMillan, Ken (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8312, 735-743 (2013).
Summary: E is a theorem prover for full first-order logic with equality. It reduces first-order problems to clause normal form and employs a saturation algorithm based on the equational superposition calculus. E is built on shared terms with cached rewriting, and employs several innovations for efficient clause indexing. Major strengths of the system are automatic problem analysis and highly flexible search heuristics. The prover can provide verifiable proof objects and answer substitutions with very little overhead. E performs well, solving more than 69% of TPTP-5.4.0 FOF and CNF problems in automatic mode.
For the entire collection see [Zbl 1277.68016].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI