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 Trackerhttps://github.com/zenon-prover/zenon/issues
MaintainerDamien Doligez <damien.doligez@inria.fr>
Dependencies
Optional dependencies
Conflicts
Source [http] https://github.com/zenon-prover/zenon/archive/0.8.5.tar.gz
md5=6c64d2c29bbcb3571f25f7f8c2dbea6c
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/zenon/zenon.0.8.5/opam
No package is dependent