Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

[Caml-list] Announce: release of Zenon

1 view
Skip to first unread message

Damien Doligez

unread,
Mar 3, 2006, 5:35:15 AM3/3/06
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

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

0 new messages