zenonversion

An Extensible Automated Theorem Prover Producing Checkable Proofs

Automated theorem prover for first order classical logic (with equality), based on the tableau method. Zenon handles first-order logic with equality. Its most important feature is that it outputs the proofs of the theorems, in Coq-checkable form.

AuthorsR. Bonichon, D. Delahaye and D. Doligez
Published
Homepagehttp://zenon-prover.org/
Issue Trackerzenon.prover at gmail.com
Maintainerhttps://github.com/ocaml/opam-repository/issues
Dependencies
Source [http] http://pkgs.fedoraproject.org/repo/pkgs/zenon/zenon-0.7.1.tar.xz/cb8b35e2d55dabcc7d8a1e8b3600f68a/zenon-0.7.1.tar.xz
sha256=0d3db37197dcd8eef559a28fec12e12e819ebcc79ad774b56bb74408971f3da9
md5=cb8b35e2d55dabcc7d8a1e8b3600f68a
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/zenon/zenon.0.7.1/opam
No package is dependent