Theorem Proving Examples

This is version 0 of the code, and you should probably download the latest version instead.

This code was written by John Harrison to accompany a textbook on automated theorem proving. It is intended to illustrate the basic ideas of a wide range of theorem proving techniques. There is no accompanying documentation, but 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.06. It 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 Camlp4.

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 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


Decidable subsets and theories

Model checking

Interactive theorem proving