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.