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.
1 comment
[ 4.8 ms ] story [ 13.2 ms ] threadAmazon 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).