This book is a good introductory catalog of automated reasoning concepts and methods. But I believe that programmers who are going to write automated reasoning systems should augment their computer knowledge (of logic) by learning a full- blown (serial, not tree) logical notation for both 1st and 2nd order predicate calculus.Solving the inference problem is NP-Complete, and computational cycles explode as the number of premisses increase. Automated methods of solving the inference problem are often O(n^2) and often infeasible, for "real-world" problems. Most programmers don't have a broad enough horizon in formal logic to quickly recognize WHEN a certain automated technique will be useful.
I suggest a symbolic logic text such as Copi's Symbolic Logic, 5th ed., and then aggressively read about optimizing methods which are currently being developed (ex. Optimization Methods for Logical Inference, Chandru et alia).
However, as an introduction, the reviewed book is excellent.
