Look up function:
FREE SOFTWARE ON CAMLCITY.ORG
"first-order automated theorem prover generating coq output"
This package contains the zenon theorem prover. Zenon is a first-order automated theorem prover with equality, based on a tableaux method. Zenon is developed by Damien Doligez at INRIA. Its main strength is that it can output a trace of its proofs in the form of a Coq script or a Coq term. In other words, its results can be checked by the Coq proof-assistant (or conversely, zenon can be seen as a powerful first-order tactic for Coq). It is also the main prover of the Focal system.
| Version: | 0.5.0 |
| Homepage: | "http://focal.inria.fr/zenon/" |
| Maintainer: | "Virgile Prevosto <virgile.prevosto@m4x.org>" |
| Files: |
bin/zenon lib/zenon/zenon.v lib/zenon/zenon.vo lib/zenon/zenon_coqbool.v lib/zenon/zenon_coqbool.vo lib/zenon/zenon_equiv.v lib/zenon/zenon_equiv.vo |
| Built from sources: |
zenon-0.5.0 |
