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 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.
- lib.ml: Utility functions
- intro.ml: Trivial example from the introduction
- formulas.ml: General type of formulas, parsing, printing etc.
Propositional logic
First order logic
Equality
Decidable subsets and theories
Model checking
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