Review
"Valuable as both a strong introduction for complete beginners and a rich reference source, even for expert logicians."
D.V. Feldman, CHOICE
" [...] if you want to implement ATP (automated theorem proving) code this book is an excellent choice. It has complete implementations of absolutely everything in OCaml (a dialect of ML, a mostly functional programming language) which is an excellent choice for this type of application."
D. Fox, amazon.com
"[...] sure to fill a need for a well-rounded work that can serve both as a reference on a range of topics and as an introductory text, especially for those who wish to study the subject for its possible practical uses. [...] Good features of the book are its overall readability, the good historical perspective conveyed while retaining its serious scholarly gravitas, and the use of OCaml to work with the concepts, presented alongside."
Shrisha Rao, Computing Reviews
"Harrison exhibits both the remarkable flexibility and limitations of OCaml (and other languages) for automated theorem proving. [...] I strongly recommend Harrison's handbook to mathematicians working on provability, computer program developers working to establish self-coherence of some parts of their programs, and students looking to understand propositional and first-order logic."
Arturo Ortiz-Tapia, Computing Reviews
"[...] the book is remarkable in many ways, including the breadth of its scope, the depth of its insights, and the clarity and readability of its prose. [...] while Harrison does focus on implementation and practical issues, he does not skimp on the underlying theory; indeed, the text passes between the two poles with surprising fluidity. The book does not assume background in logic, and appendices review the requisite background in mathematics and programming. As a result, the text is accessible to a broad audience, including sufficiently advanced undergraduates. [...] Harrison does a very good job of providing broader context and pointers to the literature. Each section ends with copious notes and references. As a result, the book can serve as a helpful introduction to the contemporary literature, like having a friendly uncle working in the field. [...] It provides a lucid and synoptic overview of these topics, conveys a solid theoretical background, provides tools for experimentation, and offers notes and pointers that facilitate a smooth transition to the contemporary literature. [...] Anyone working in automated reasoning, or looking to come up to speed on developments in the field, will want to have a copy at hand."
Jeremy Avigad, Theory and Practice of Logic Programming
"Overall this is an excellent book that provides a wide-ranging view on automated reasoning techniques for classical logic. The author achieves a good balance between providing good intuition and rigour in presenting the selected materials. Its breadth will make sure that even an expert in the area will find something useful in the book."
Alwen Tiu, The Bulletin of Symbolic Logic
Book Description
A one-stop reference, self-contained, with theoretical topics presented in conjunction with implementations for which code is supplied.
About the Author
John Harrison is a Principal Engineer at the Intel Corporation in Portland, Oregon. He specialises in formal verification, automated theorem proving, floating-point arithmetic and mathematical algorithms.
