References

Links

Nearly all of my scientific papers, many of which deal with aspects of E, are available at my bibliography page.
E has an article on Wikipedia.
The TPTP library is used for testing and defines the standards for input and output.
The CADE ATP System Competition (CASC) is a yearly event for the comparison of fully automated theorem provers.
Waldmeister is a theorem prover for unit equality that has pioneered a number of techniques lifted to full first order logic in E.
Vampire is a leading theorem prover for first-order (and now also higher-order) logic.
SPASS is another theorem prover for first-order logic and probably the first high-performance implementation of the Superposition calculus proper.

References

If you use E and want to reference it, the latest (short) overview is [SCV:CADE-2019].

[AHL:JSC-2003]

Jürgen Avenhaus, Thomas Hillenbrand, and Bernd Löchner. On Using Ground Joinable Equations in Equational Theorem Proving. Journal of Symbolic Computation, 36(1-2):217–233, 2003.

[BG94]

L. Bachmair and H. Ganzinger. Rewrite-Based Equational Theorem Proving with Selection and Simplification. Journal of Logic and Computation, 3(4):217–247, 1994.

[DKS97]

J. Denzinger, M. Kronenburg, and S. Schulz. DISCOUNT: A Distributed and Learning Equational Prover. Journal of Automated Reasoning, 18(2):189–198, 1997. Special Issue on the CADE 13 ATP System Competition.

[Loechner:JAR-2006]

Bernd Löchner. Things to Know when Implementing KBO. Journal of Automated Reasoning, 36(4):289–310, 2006.

[Loechner:IJAIT-2006]

Bernd Löchner. Things to Know When Implementing LPO. International Journal on Artificial Intelligence Tools, 15(1):53–80, 2006.

[NW:SmallCNF-2001]

A. Nonnengart and C. Weidenbach. Computing Small Clause Normal Forms. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 5, pages 335–367. Elsevier Science and MIT Press, 2001.

[RV:IJCAI-2001]

A. Riazanov and A. Voronkov. Splitting without Backtracking. In B. Nebel, editor, Proc. of the 17th International Joint Conference on Artificial Intelligence (IJCAI-2001), Seattle, volume 1, pages 611–617. Morgan Kaufmann, 2001.

[Schulz:AICOM-2002]

S. Schulz. E – A Brainiac Theorem Prover. Journal of AI Communications, 15(2/3):111–126, 2002.

[Schulz:FVI-2013]

S. Schulz. Simple and Efficient Clause Subsumption with Feature Vector Indexing. In Maria Paola Bonacina and Mark E. Stickel, editors, Automated Reasoning and Mathematics: Essays in Memory of William W. McCune, Springer, 2013.

[Schulz:IJCAR-2012]

S. Schulz. Fingerprint Indexing for Paramodulation and Rewriting. In Bernhard Gramlich, Ulrike Sattler and Dale Miller, editors, Proc. of the 6th IJCAR, Manchester, United Kingdom, 2012.

[Schulz:LPAR-2013]

S. Schulz. System Description: E 1.8. In Ken McMillan, Aart Middeldorp and Andrei Voronkov, editors, Proc. of the 19th LPAR, Stellenbosch, South Africa, 2013.

[SCV:CADE-2019]

Stephan Schulz, Simon Cruanes, Petar Vukmirovic: Faster, Higher, Stronger: E 2.3, Proceedings of the 27th Conference on Automated Deduction (CADE'19), Natal, Brazlil. Volume 11716 of LNAI. Springer, 2019.

[Sutcliffe:JAR-2009]

G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning 43(4):337-363, 2009.

[VBS:TACAS-2023]

Petar Vukmirovic, Jasmin Christian Blanchette and Stephan Schulz. Extending a High-Performance Prover to Higher-Order Logic. Proc. 29th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23), Paris, France, 2023