* Announce: release of Zenon
@ 2006-03-03 10:32 Damien Doligez
0 siblings, 0 replies; only message in thread
From: Damien Doligez @ 2006-03-03 10:32 UTC (permalink / raw)
To: caml users
Greetings,
It is my pleasure to announce 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.4.1, available at < http://focal.inria.fr/zenon/ >.
Unfortunately, there is no documentation yet, so this is for the
adventurous spirit.
It is released under the New BSD license.
-- Damien
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2006-03-03 10:31 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2006-03-03 10:32 Announce: release of Zenon Damien Doligez
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).