[17] Automated Deduction/Theorem Proving

   C. Chang and R.C. Lee, "Symbolic Logic and Mechanical Theorem
   Proving", Academic Press, 1973.

   Alan Bundy, "The Computer Modelling of Mathematical Reasoning",
   Academic Press, 1983. [Contains Prolog code for a simple
   resolution-based theorem prover.]

   David Duffy, "Principles of Automated Theorem Proving", John
   Wiley and Sons, 1991. 

   Larry Wos and Ross Overbeek and Ewing Lusk and Jim Boyle,
   "Automated Reasoning. Introduction and Applications",  Second Edition,
   McGraw-Hill, 1992.

   Proceedings of the 11th International Conference on Automated
   Deduction (CADE-11), D. Kapur (editor), Saratoga Springs, NY, USA,
   June 15-18, 1992, Lecture Notes in AI 607, Springer-Verlag, 1992, 793
   pages.  ISBN 0-387-55602-8 and 3-540-55602-8.
    [The CADE proceedings have a systems abstracts section with short
     descriptions of implemented systems, many of which are available
     by anonymous ftp.]