* [Caml-list] [Announce] Release 0.8.0 of Zenon
@ 2014-10-21 9:58 François Pessaux
0 siblings, 0 replies; only message in thread
From: François Pessaux @ 2014-10-21 9:58 UTC (permalink / raw)
To: caml-list, focalize-devel FoCaLize-Devel, focalize-users FoCaLiZe-Users
[-- Attachment #1: Type: text/plain, Size: 663 bytes --]
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
[-- Attachment #2: Type: text/html, Size: 1415 bytes --]
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2014-10-21 9:58 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2014-10-21 9:58 [Caml-list] [Announce] Release 0.8.0 of Zenon François Pessaux
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox