The code available on this page was written by John Harrison to accompany his textbook
on logic and automated theorem proving, published in March 2009 by Cambridge
University Press. For more information about the book, click the picture on the
right. As well as the code, this page includes links to other relevant
resources, which at the moment is the following:
An SML version of the
interactive theorem proving part of code is also available! Thanks to
Anders Schlichtkrull and Jørgen Villadsen.
"[...] 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."
"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."
"Computer science has now transformed the practice of mathematical logic [...] the present introduction to first-order logic stands apart from its 20th-century antecedents by dint of thoroughly integrating a computation perspective almost from the first page [...] Valuable as both a strong introduction for complete beginners and a rich reference source, even for expert logicians. [...] Highly recommended."
"[...] 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."
"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."
"[...] 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."
"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."
"This book is an excellent introduction into the world of automated theorem proving. The author takes it slowly, building up from the very basics, but the book is still very complete and covers most relevant topics [...] Harrison's book is also complete in the sense that there's an implementation for every algorithm described in this book (so, you'll have a hard time finding a handwavy description). [...] While reading the book you can basically build your own automated theorem prover from scratch. [...] Finally, I really like Harrison's writing style. It's always a joy to read this book, and it's very much to the point and never over-burdened (but there are many cross-references if you want to dig deeper). This book is a 'must-have' for everyone who's interested in automated decision procedures."
"The style, far from that of a reference book, is deeply pedagogical, complete with a significant set of well-crafted exercises. It is well written using lucid prose, with the author taking great pains to elicidate important points, pausing to illustrate some subtleties, as well as being rather erudide in its treatment of the relevant literature, both historical and contemporary. As a textbook style introduction to the theory and practice of (first order, mathematical) logic and automated reasoning it succeeds beautifully. The textbook masterfully weaves together theory and practice. [...] It would be easy to imagine using this book for several courses on logic, theorem proving, and decision procedures, from an introductory course to several Master's level advanced courses. There is in fact so much material here that one could probably create a whole stream, (say of 4 courses) in an undergraduate curriculum for specializing in mechanized mathematics. Any researcher who wantes to learn how simple theorem proving systems are built would greatly benefit from reading this book."
.All code is written in Objective CAML, and has been tested with version 3.09.3. If you want to use it with OCaml versions 3.10 and above, you will also need the camlp5 preprocessor (>= 4.07), but for older versions the built-in camlp4 works. The code can either be loaded interactively into the toplevel system for experimentation or compiled into bytecode or native code. Thanks to Daniel de Rauglaudre for help with camlp5.
The code is not intended to be efficient and isn't likely to be much use for serious applications. Nevertheless I would be happy if anyone does find it useful. Please see the file LICENSE.txt first. Note also that Stålmarck's method (file stal.ml) is protected by patents covering commercial use.
Page last updated Friday 8th January 2016.