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://zenon-prover.org/zenon-0.8.0.tar.gz sha256=807d946af0295f54edd76ee5ec0563f85a307d7a6b313f98fe6942b32f80ec87 md5=4d82ae5b6dc498a73ef85a353c5da325 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/zenon/zenon.0.8.0/opam |
No package is dependent
