Extensible Automated Theorem Prover
Zenon is an Extensible Automated Theorem Prover Producing Checkable Proofs
Zenon is an automated theorem prover for first order classical logic (with equality), based on the tableau method.
Zenon is intended to be the dedicated prover of the Focal environment, an object-oriented algebraic specification and proof system, which is able to produce OCaml code for execution and Coq code for certification.
released on 6 June 2016
|License||Verified by||Verified on||Notes|
|License:BSD 3Clause||BABA200||25 February 2017|
Leaders and contributors
Resources and communication
|Required to use||OCaml 3.08.x or 3.09.x (with ocamlopt)|
|Required to use||Coq 8.0.x|
This entry (in part or in whole) was last reviewed on 25 February 2017.