One of my colleague complained about the fact that my list currently lacks of books about logic and theorem proving…
Of course, he’s right ! Shame on me ! That’s why I will start introducing a few books about this topic (starting from now).
So, the “Handbook of Practical Logic and Automated Reasoning” has been a long awaited one. Its author took about ten years to complete it… but I would say it really worth it.
The book cover all the basic topics about logic (from propositional up to first order logic) and give some hints on how to go a bit further (higher order logic). All along the chapters, logical concepts, proof techniques and tactics are illustrated and implemented using OCaML code. Moreover, the author is really crystal clear and pedagogic in its explanations. I would say it is an excellent introduction, both, to logic and to proof assistants and their internals. Though, I would warn people which are not familiar with mathematics and, more precisely, with logic that it might require a bit of work to start with. But any, even extremely basic, course on logic will make it.
Handbook of Practical Logic and Automated Reasoning, by John Harrison published by Cambridge University Press (2009).