This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

[Caml-list] Theorem proving example code available
• Harrison, John R
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2003-05-20 (23:57) From: Harrison, John R Subject: [Caml-list] Theorem proving example code available
```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

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@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.

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

```