Theorem Proving Examples

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 stal.ml) is protected by patents covering commercial use.

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.
• lib.ml: Utility functions
• intro.ml: Trivial example from the introduction
• formulas.ml: General type of formulas, parsing, printing etc.

Interactive theorem proving

• lcf.ml: LCF-style system for equational logic
• hilbert.ml: Hilbert-style system for first order logic
• lcfprop.ml: Propositional logic by inference
• lcffol.ml: First-order reasoning by inference
• checking.ml: Checking automatic tableau proofs in LCF
• tactics.ml: Tactics and Mizar-style proofs

Miscellaneous

• sigma.ml: Prover for sigma-sentences etc.
• turing.ml: Turing machines etc.
• undecidable.ml: Other code related to undecidability
• bhk.ml: BHK interpretation and Curry-Howard (trivial ML example)
• many.ml: Many-sorted logic (trivial motivating example)
• hol.ml: Higher order logic