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.
| Authors | R. Bonichon, D. Delahaye and D. Doligez |
|---|---|
| Published | |
| Homepage | http://zenon-prover.org/ |
| Issue Tracker | zenon.prover at gmail.com |
| Maintainer | https://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 md5=cb8b35e2d55dabcc7d8a1e8b3600f68a |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/zenon/zenon.0.7.1/opam |
No package is dependent
