Opam Package zenon.0.8.5

Package info

opam-namezenon
opam-version0.8.5
synopsisAn Extensible Automated Theorem Prover Producing Checkable Proofs
description Automated theorem prover for first order classical logic (with equality), based on the tableau method. Zenon handles first-order logic with equality. Its most important feature is that it outputs the proofs of the theorems, in Coq-checkable form.
authors
  • R. Bonichon
  • D. Delahaye
  • D. Doligez
homepagehttp://zenon-prover.org/
deps (2)
revdeps(0)
metas(0)
libraries(0)

Package modules

Package sources

zenon

Package files

lib/zenon/zenon_induct.vo
lib/zenon/zenon_induct.v
lib/zenon/zenon_focal.vo
lib/zenon/zenon_focal.v
lib/zenon/zenon_equiv.vo
lib/zenon/zenon_equiv.v
lib/zenon/zenon_coqbool.vo
lib/zenon/zenon_coqbool.v
lib/zenon/zenon.vo
lib/zenon/zenon.v
lib/zenon
bin/zenon