Greetings,

It is my pleasure to announce (for Damien Doligez ^_^) the release of Zenon,

an automatic theorem prover written in OCaml.

Zenon handles first-order logic with equality.  Its most important feature is

that it outputs the proofs of the theorems, in Coq-checkable form.

This is version 0.8.0, available at < http://sosie.inria.fr > (and soon

at  < http://zenon-prover.org >) with several issues fixed since the

last release.

Unfortunately, there is no documentation yet, so this is for the

adventurous spirit.

It is released under the New BSD license.