References

Not done yet.

[Bachmair-Ganzinger-res]

L. Bachmair and H. Ganzinger. "Resolution Theorem Proving". Chapter 2 in Handbook of Automated Reasoning (ed. A. Robinson and A. Voronkov), 2001. Preliminary version.

[Nieuwenhuis-Rubio-para]

R. Nieuwenhuis and A. Rubio. "Paramodulation-Based Theorem Proving". Chapter 7 in Handbook of Automated Reasoning (ed. A. Robinson and A. Voronkov), 2001.

[Champeaux-miniscope]

D. Champeaux. "Sub-problem finder and instance checker, two cooperating modules for theorem provers". J. ACM, 33(4):633--657, 1986.

[Dershowitz-termination]

N. Dershowitz. "Termination of rewriting". J. Symbolic Computation, 3:69-116, 1987.

[McCune-Otter33]

W. McCune. Otter 3.3 Reference Manual. Tech. Memo ANL/MCS-TM-263, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, August 2003.

[McCune-Mace4]

W. McCune. Mace4 Reference Manual and Guide. Tech. Memo ANL/MCS-TM-264, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, August 2003.

[RV-lrs]

A. Riazanov and A. Voronkov. "Limited resource strategy in resolution theorem proving". J. Symbolic Computation, 36(1-2):101-115, 2003.

[Veroff-hints]

R. Veroff. "Using hints to increase the effectiveness of an automated reasoning program: Case studies". J. Automated Reasoning, 16(3):223--239, 1996.

[Veroff-sketches]

R. Veroff. "Solving open questions and other challenge problems using proof sketches". J. Automated Reasoning, 27(2):157--174, 2001.