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 <http://sosie.inria.fr/> > (and soon
at  < http://zenon-prover.org <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.

 — François for Damien