zenon

AuthorsR. Bonichon, D. Delahaye and D. Doligez
Homepagehttp://zenon-prover.org/
Issue Trackerzenon.prover at gmail.com
Maintainerhttps://github.com/ocaml/opam-repository/issues
Dependencies
coq
PublishedMay 26, 2015
Source [http] http://zenon-prover.org/zenon-0.8.0.tar.gz
4d82ae5b6dc498a73ef85a353c5da325
StatisticsInstalled 7 times last month.
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/zenon/zenon.0.8.0/opam

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.

No package is dependent