zenon 0.7.1
| Maintainer | contact@ocamlpro.com | ||||
|---|---|---|---|---|---|
| Dependencies |
|
||||
| Published | Aug 21, 2012 | ||||
| Source [http] |
http://focal.inria.fr/zenon/zenon-0.7.1.tar.gz a8b9689b51d2f649f8eeb29a2b9bbae8 |
||||
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/zenon/zenon.0.7.1/opam | ||||
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 |