Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Theorem Proving Examples

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

For an earlier version of this code, including some additional material like model checking, see here. However, the present code is generally cleaner and has a better Makefile.

All code is written in Objective CAML, and has been tested with version 3.09.3. If you want to use it with OCaml versions 3.10 and above, you will also need the camlp5 preprocessor (>= 4.07), but for older versions the built-in camlp4 works. The code 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 camlp5.

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

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

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
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
real.ml: Real quantifier elimination
grobner.ml: Gröbner bases
geom.ml: Geometry theorem proving
interpolation.ml: Constructive Craig/Robinson interpolation
combining.ml: Combined decision procedure

Interactive theorem proving

lcf.ml: LCF-style system for first order logic
lcfprop.ml: Propositional logic by inference
folderived.ml: First-order reasoning by inference
lcffol.ml: LCF implementation of first-order tableaux
tactics.ml: Tactics and Mizar-style proofs

Miscellaneous

limitations.ml: Various code related to undecidability