The author of this book is John Harrison of Intel, where his knowledge of automatic proofs is used in optimally designing chipsets. He is also the author of HOL Light (
http://www.cl.cam.ac.uk/~jrh13/hol-light/), a program that helps users prove mathematical theorems. The submission is a book that he published in 2009 describing automated proofs, with a full implementation in OCaml. When I was doing grad work back in 2007-2008, the source code that went along with this book was invaluable in my work. I'm surprised that I haven't seen much discussion about this book, which is definitely worth checking out.
Amazon has a few good reviews (http://www.amazon.com/Handbook-Practical-Logic-Automated-Rea...), and a CMU faculty member wrote an extensive review (http://www.andrew.cmu.edu/user/avigad/Reviews/harrison.pdf).