[Bac98] L. Bachmair. Personal communication at CADE-15, Lindau. Unpublished, 1998.
[BDP89] L. Bachmair, N. Dershowitz, and D.A. Plaisted. Completion Without Failure. In H. Ait-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 2, pages 1–30. Academic Press, 1989.
[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.
[CL73] C. Chang and R.C. Lee. Symbolic Logic and Mechanical Theorem Proving. Computer Science and Applied Mathematics. Academic Press, 1973.
[Der91] N. Dershowitz. Ordering-Based Strategies for Horn Clauses. In J. Mylopoulos, editor, Proc. of the 12th IJCAI, Sydney, volume 1, pages 118–124. Morgan Kaufmann, 1991.
[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.
[DS94a] J. Denzinger and S. Schulz. Analysis and Representation of Equational Proofs Generated by a Distributed Completion Based Proof System. Seki-Report SR-94-05, Universität Kaiserslautern, 1994.
[DS94b] J. Denzinger and S. Schulz. Recording, Analyzing and Presenting Distributed Deduction Processes. In H. Hong, editor, Proc. 1st PASCO, Hagenberg/Linz, volume 5 of Lecture Notes Series in Computing, pages 114–123, Singapore, 1994. World Scientific Publishing.
[DS96] J. Denzinger and S. Schulz. Recording and Analysing Knowledge-Based Distributed Deduction Processes. Journal of Symbolic Computation, 21(4/5):523–541, 1996.
[HBF96] Th. Hillenbrand, A. Buch, and R. Fettig. On Gaining Efficiency in Completion-Based Theorem Proving. In H. Ganzinger, editor, Proc. of the 7th RTA, New Brunswick, volume 1103 of LNCS, pages 432–435. Springer, 1996.
[HJL99] Th. Hillenbrand, A. Jaeger, and B. Löchner. System Abstract: Waldmeister – Improvements in Performance and Ease of Use. In H. Ganzinger, editor, Proc. of the 16th CADE, Trento, volume 1632 of LNAI, pages 232–236. Springer, 1999.
[McC94] W.W. McCune. Otter 3.0 Reference Manual and Guide. Technical Report ANL-94/6, Argonne National Laboratory, 1994.
[MIL+97] M. Moser, O. Ibens, R. Letz, J. Steinbach, C. Goller, J. Schumann, and K. Mayr. SETHEO and E-SETHEO – The CADE-13 Systems. Journal of Automated Reasoning, 18(2):237–246, 1997. Special Issue on the CADE 13 ATP System Competition.
[MW97] W.W. McCune and L. Wos. Otter: The CADE-13 Competition Incarnations. Journal of Automated Reasoning, 18(2):211–220, 1997. Special Issue on the CADE 13 ATP System Competition.
[NN93] P. Nivela and R. Nieuwenhuis. Saturation of First-Order (Constrained) Clauses with the Saturate System. In C. Kirchner, editor, Proc. of the 5th RTA, Montreal, volume 690 of LNCS, pages 436–440. Springer, 1993.
[RV01] A. Riazanov and A. Voronkov. Vampire 1.1 (System Description). In R. Goré, A. Leitsch, and T. Nipkow, editors, Proc. of the 1st IJCAR, Siena, volume 2083 of LNAI, pages 376–380. Springer, 2001.
[RV02] A. Riazanov and A. Voronkov. The Design and Implementation of VAMPIRE. Journal of AI Communications, 15(2/3):91–110, 2002.
[Sch99] S. Schulz. The E Web Site. http://www4.informatik.tu-muenchen.de/\-$\sim$schulz/\-WORK/\-eprover.html, 1999.
[Sch00] S. Schulz. Learning Search Control Knowledge for Equational Deduction. Number 230 in DISKI. Akademische Verlagsgesellschaft Aka GmbH Berlin, 2000. Ph.D. Thesis, Fakultät für Informatik, Technische Universität München.
[Sch01] S. Schulz. Learning Search Control Knowledge for Equational Theorem Proving. In F. Baader, G. Brewka, and T. Eiter, editors, Proc. of the Joint German/Austrian Conference on Artificial Intelligence (KI-2001), volume 2174 of LNAI, pages 320–334. Springer, 2001.
[Sch02] S. Schulz. E – A Brainiac Theorem Prover. Journal of AI Communications, 15(2/3):111–126, 2002.
[Sch04] S. Schulz. System Description: E 0.81. In D. Basin and M. Rusinowitch, editors, Proc. of the 2nd IJCAR, Cork, Ireland, volume 3097 of LNAI, pages 223–228. Springer, 2004.
[SSCG06] Geoff Sutcliffe, Stephan Schulz, Koen Claessen, and Allen Van Gelder. Using the TPTP Language for Writing Derivations and Finite Interpretations . In Ulrich Fuhrbach and Natarajan Shankar, editors, Proc. of the 3rd IJCAR, Seattle, volume 4130 of LNAI, pages 67–81, 4130, 2006. Springer.
[Sut05] G. Sutcliffe. The TPTP Web Site. http://www.tptp.org, 2004–2005.
[Tam97] T. Tammet. Gandalf. Journal of Automated Reasoning, 18(2):199–204, 1997. Special Issue on the CADE 13 ATP System Competition.
[WAB+99] C. Weidenbach, B. Afshordel, U. Brahm, C. Cohrs, T. Engel, G. Jung, E. Keen, C. Theobalt, and D. Topic. System Abstract: SPASS Version 1.0.0. In H. Ganzinger, editor, Proc. of the 16th CADE, Trento, volume 1632 of LNAI, pages 378–382. Springer, 1999.
[Wei99] C. Weidenbach. Personal communication at CADE-16, Trento. Unpublished, 1999.
[Wei01] C. Weidenbach. SPASS: Combining Superposition, Sorts and Splitting. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 27, pages 1965–2013. Elsevier Science and MIT Press, 2001.
[WGR96] C. Weidenbach, B. Gaede, and G. Rock. SPASS & FLOTTER Version 0.42. In M.A. McRobbie and J.K. Slaney, editors, Proc. of the 13th CADE, New Brunswick, volume 1104 of LNAI, pages 141–145. Springer, 1996.