Handbook of Automated Reasoning

Rating:
Summary: Required reading for ATP researchers
Review: I've found this to be the best introduction to (mostly classical) automated theorem proving. The matter is clearly presented and can be understood even by non-logicians. In the first part of the book there is a solid treatment of classical theorem proving, including an excellent chapter on tableau based methods. In the second part there is a short treatment of intuitionistic theorem proving, and some throwaway discussion of the relation of theorem proving and type-theory (specifically, dependent type-theories as used in Logical Frameworks), model checking, verification, etc. I give the book 4 stars because of its well-rounded discussion of classical theorem proving, and hold back the last star because the material is a bit dated compared to modern research directions, and doesn't cover intuitionistic theorem proving in great detail.