Best introductory book on automated theorem proving available. Although it was written in the early 70's, it is written in a very clear, but mathematically precise, manner. It does not drown a reader with an abundance of symbols and definitions. It is a clear and well written exposition on automated theorem proving based on resolution. Unlike some recent text books, it does NOT use sequentzen logic systems. It covers all aspects of resolution-based theorem proving: different forms of resolution, deletion strategies, unification.

If you are interested in Artificial Intelligence or you are one of those crazy guys who likes the Computer theory area this is a good book for you, mechanical theorem proving is an important subject into the AI area, all you want to know is Mathematical Logic, first order logic and predicate calculus. Very good book but very hard too (specially if you have to make some Mechanical theorem provers by yourself as a school project :) )