Edited by Robert Veroff.

MIT Press, 1997, ISBN 0-262-22055-5.

- Larger image of the cover.
- Previous version of the cover (I chickened out!).
- MIT Press page for the book.

*Wos and Automated Deduction at ANL: The Ethos*

Ross Overbeek and Ewing Lusk*A Completeness Result for Linked Resolution*

Kenneth Kunen*Generic Automatic Proof Tools*

Lawrence C. Paulson*Automated Generation of Construction Steps for Geometric Constraint Problems*

S. Chou, Xiao-Shan Gao, and Jing-Zhong Zhang*33 Basic Test Problems: A Practical Evaluation of Some Paramodulation Strategies*

William Mccune*Specifying Latin Square Problems in Propositional Logic*

Hantao Zhang*Mechanized Formal Reasoning about Programs and Computing Machines*

Robert S. Boyer and J Strother Moore*Constructors Can Be Partial, Too*

Deepak Kapur*Metalevel Reasoning for Controlling Automated Reasoning Programs*

Lawrence J. Henschen