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