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.

- LICENSE.txt: Please read before using
- make.ml: Load code interactively into OCaml toplevel
- Makefile: Build executable or byte code
- example.ml: Example of using compiled code

- lib.ml: Utility functions
- intro.ml: Trivial example from the introduction
- formulas.ml: General type of formulas, parsing, printing etc.

- prop.ml: Basic propositional logic stuff
- propexamples.ml: Generate tautologies from circuits etc.
- defcnf.ml: Definitional CNF
- dp.ml: Davis-Putnam procedure
- stal.ml: Stålmarck's algorithm
- bdd.ml: Binary decision diagrams

- fol.ml: Basic first order logic stuff
- skolem.ml: Prenex and Skolem normal forms
- herbrand.ml: Herbrand theorem and mechanization
- unif.ml: Unification algorithm
- tableaux.ml: Tableaux
- resolution.ml: Resolution
- prolog.ml: Horn clauses and Prolog
- meson.ml: MESON-type model elimination
- skolems.ml: Skolemizing a set of formulas (theoretical)

- equal.ml: Naive equality axiomatization
- cong.ml: Congruence closure
- rewrite.ml: Rewriting
- order.ml: Simple term orderings including LPO
- completion.ml: Knuth-Bendix completion
- orewrite.ml: Ordered rewriting
- eqelim.ml: Equality elimination: Brand transform etc.
- paramodulation.ml: Paramodulation.

- decidable.ml: Some decidable subsets of first-order logic
- qelim.ml: Quantifier elimination basics
- cooper.ml: Cooper's algorithm for Presburger arithmetic
- complex.ml: Complex quantifier elimination
- grobner.ml: Gröbner bases
- real.ml: Real quantifier elimination
- geom.ml: Geometry theorem proving
- interpolation.ml: Constructive Craig/Robinson interpolation
- combining.ml: Combined decision procedure

- transition.ml: Finite state transition systems
- temporal.ml: Linear temporal logic
- model.ml: CTL model checking
- ltl.ml: LTL decision procedure
- ste.ml: Symbolic trajectory evaluation

- 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