Docs GODI Archive
Projects Blog Link DB

Look up function:

(e.g. "List.find" or "keysym")
More options

FREE SOFTWARE ON CAMLCITY.ORG

GODI Package apps-zenon

"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
This web site is published by Informatikbüro Gerd Stolpmann
Powered by Caml