Robinson, J. (1965). A machine oriented logic based on the resolution principle. Journal of the ACM, 12 (1).

Schumann, J. (1994). Delta - a bottom-up preprocessor for top-down theorem provers.

system abstract. In Proceedings of CADE-12, pp. 774-777. Springer, LNAI 814.

Stickel, M. (1988). A prolog technology theorem prover: Implementation by an extended prolog compiler. Journal of Automated Reasoning, 4, 353–380.

Stickel, M. (1994). Upside-down meta-interpretation of the model elimination theoremproving procedure for deduction and abduction. Journal of Automated Reasoning, 13, 189-210.

Sutcliffe, G. (1992). A heterogeneous parallel deduction system. In Proceedings of FGCS'92 Workshop W3.

Sutcliffe, G., & Suttner, C. (1998). The TPTP problem library: CNF release v1.2.1. Journal of Automated Reasoning, 21, 177–203.

Sutcliffe, G., & Suttner, C. (1997). The results of the CADE-13 ATP system competition.

Journal of Automated Reasoning, 18 (2), 271–286.

Sutcliffe, G., Suttner, C., & Yemenis, T. (1994). The TPTP problem library. In Proceedings of CADE-12, pp. 252-266. LNA1 814.

Tammet, T. (1997). Gandalf. Journal of Automated Reasoning, 18 (2), 199–204. Weidenbach, C., Gaede, B., & Rock, G. (1996). Spass & Flotter Version 0.42. In Proc.

CADE-13, pp. 141-145. Springer, LNAI 1104.

Wolf, A., & Fuchs, M. (1997). Cooperative parallel automated theorem proving.

l n Schnekenburger, T., & Stellner, G. (Eds.), Dynamic Load Distribution for Parallel Applications, pp. 129-145. Teubner.