Code and resources for "Handbook of Practical Logic and Automated Reasoning"

(cover of HOPLAR) 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 just the following: The code is used in the book to explain and demonstrate a wide range of theorem proving techniques. It is designed to be used in conjunction with the book, and there is no other accompanying documentation. However, it can be used independently: at least the code is commented and there are examples illustrating most of the techniques in the corresponding files listed below. If you have any comments, corrections or suggestions about how the clarity of parts of the code could be improved, I'd be very happy to hear from you. Please email me at .

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.

The key places to start

All the code together

All the files mentioned below together with the Makefile etc., packaged together as a gzipped tar file, can be downloaded here.

Individual files

The following files are basic background and libraries. The main body of the code is split into several groups below.

Propositional logic

First order logic

Equality

Decidable subsets and theories

Interactive theorem proving

Miscellaneous

For an earlier version of this code, including some additional material like model checking, see here. However, the present code is generally cleaner and has a better Makefile.

Page last updated Friday 30th October 2009.