Fuchs, M. (1997). Flexible proof-replay with heuristics. In Proceedings of EPIA '97, pp.

1-12. Springer, LNAI 1323.

Fuchs, M. (1998a).  Relevancy-based lemma selection for model elimination using lazy

tableaux enumeration. In Proceedings of ECAI-98, pp. 346–350. John Wiley & Sons, Ltd.
Fuchs, M. (1998b). System abstract: Similanty-based lemma generation for model elimination. In Proceedings of CADE-15, pp. 33–37. Springer, LNAI 1421.

Fuchs, M. (1999). Lemma generation for model elimination by combining top-down and bottom-up inference. In Proceedings of IJCAI-99. Morgan Kaufmann, to appear.

Harrison, J. (1996). Optimizing proof search in model elimination. In Proceedings of CADE-
13, pp. 313–327. Springer, LNAI 1104.

Hasegawa, R., Inoue, K., Ohta, Y., & Koshimura, M. (1997). Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving. In Proceedings of CADE-14, pp. 176–190. Springer, LNAI 1249.

Iwanuma, K. (1997). Lemma matching for a PTTP-based top-down theorem prover. In Proceedings of CADE-14, pp. 146–160. Springer, LNAI 1249.

Korf, R. E. (1985). Depth-first iterative-deepening: An optimal admissible tree search. AI,
27, 97 - 109. Elsevier Publishers B.V. (North-Holland).

Letz, R., Mayr, K., & Goller, C. (1994). Controlled integration of the cut rule into connection tableau calculi. Journal of Automated Reasoning, 13, 297-337.

Letz, R., Schumann, J., Bayerl, S., & Bibel, W. (1992). SETHEO: A high-performance theorem prover. Journal of Automated Reasoning, 8 (2), 183–212.

Loveland, D. (1968). Mechanical theorem-proving by model elimination. Journal of the ACM, 15 (2).

Loveland, D. (1978). Automated Theorem Proving: a Logical Basis. North-Holland.

Loveland, D., Reed, D., & Wilson, D. (1995). SATCHMORE: SATCHMO with RElevancy.

Journal of Automated Reasoning, 14, 325–351.

Markovitch, S., & Scott, P. (1993). Information filtering: Selection mechanisms in learning systems. Machine Learning, 10 (2), 113-151.

Minton, S. (1990). Quantitative results concerning the utility of explanation-based learning.

Artificial Intelligence, 42, 363-391. Elsevier Science Publishers.

Moser, M., Ibens, O., Letz, R., Steinbach, J., Goller, C., Schumann, J., & Mayr, K. (1997).

The model elimination provers SETHEO and E-SETHEO. Journal of Automated Reasoning, 18 (2).