The Coq mailing list

[John R Harrison <johnh AT ichips.intel.com>]

I've made available some simple implementations of common automated
theorem proving methods. This code, intended to accompany a textbook on
theorem proving, is written in Objective CAML and covers quite a range
of techniques, e.g.

 * The Davis-Putnam procedure
 * Stalmarck's method
 * Binary decision diagrams
 * Tableaux
 * Resolution
 * Model elimination
 * Congruence closure
 * Rewriting
 * Knuth-Bendix completion
 * Brand's transformation
 * Paramodulation
 * Quantifier elimination over Z, C and R
 * Groebner bases
 * Geometry theorem proving
 * The Nelson-Oppen combination method
 * CTL and LTL model checking
 * Symbolic trajectory evaluation
 * Interactive LCF proof
 * Mizar-like proofs

For more details, and to browse or download the code, see:

  http://www.cl.cam.ac.uk/users/jrh/atp/index.html

The code is intended to illustrate the techniques described in the
simplest way I could think of, and *not* to be efficient or practically
useful. Part of my aim in making it available is to solicit ideas about
how it might be made simpler and clearer. Any suggestions will be
gratefully received at 
<johnh AT ichips.intel.com>.
 I might mention two
notable features of the code as it stands:

 o The code is entirely functional (well, excluding various status
   messages that are emitted). In fact, I cheekily redefine the OCaml
   assignment operator ":=". On the whole, this seems fine, except for
   some messiness when threading BDD state (e.g. the files "bdd.ml" and
   "model.ml").

 o To represent sets, I use canonically ordered lists. This is
   questionable both on grounds of abstraction and efficiency, but
   there is a certain convenience in having an easy concrete syntax
   and being able to pick out elements by pattern matching.

John.