Discussion:
[Announce] Release 0.8.0 of Zenon
François Pessaux
2014-10-21 09:58:55 UTC
Permalink
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
--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
Loading...