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.

The key places to start

• 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

All the code together

Individual files

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

Propositional logic

• 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

First order logic

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

Equality

• 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 subsets and theories

• 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

Model checking

• 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

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