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 | https://github.com/zenon-prover/zenon/issues |
| Maintainer | Damien Doligez <[email protected]> |
| Dependencies |
|
| Optional dependencies | |
| Conflicts | |
| Source [http] | https://github.com/zenon-prover/zenon/archive/0.8.5.tar.gz sha256=73811276ad0aa46e91e346bf38937d37b1b9930e0b9f6b0aa20a5c1959e3006e md5=6c64d2c29bbcb3571f25f7f8c2dbea6c |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/zenon/zenon.0.8.5/opam |
No package is dependent
