|Published||May 26, 2015|
|Statistics||Installed 14 times in last month.|
Automated theorem prover for first order classical logic (with equality), based on the tableau method
Zenon is an automatic theorem prover written in OCaml. 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|