1. Nearly all of my scientific papers, many of which deal with aspects of E, are available at my bibliography page.

  2. E has an article on Wikipedia.

  3. The TPTP library is used for testing and defines the standards for input and output.

  4. The CADE ATP System Competition (CASC) is a yearly event for the comparison of fully automated theorem provers.

  5. Waldmeister is a theorem prover for unit equality that has pioneered a number of techniques lifted to full first order logic in E.

  6. Vampire is a leading theorem prover for first-order logic.

  7. SPASS is another theorem prover for first-order logic and probably the first high-performance implementation of the Superposition calculus.


If you use E and want to reference it, the latest (short) overview is [Schulz:LPAR-2013].


  1. 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.


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


  1. 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.


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


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


  1. 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.


  1. 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.


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


  1. 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.   


  1. 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 .   


  1. 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.