Mechanical theorem proving is an important subject in artificial intelligence. It has been applied to many areas--program analysis, program synthesis, deductive question-answering systems, problem-solving systems, and robot technology. This classic text provides a thorough discussion of mechanical theorem proving and its applications as well as an introduction to symbolic logic. A purely model-theoretic approach to first-order logic is adopted, and the book emphasizes efficient computer implementations of proof techniques. Appropriate for both undergraduates and graduate courses in theorem proving, this text is also suitable as a supplementary textbook in artificial intelligence to provide the student with a background in mechanical theorem proving and application areas.