package zenon
An Extensible Automated Theorem Prover Producing Checkable Proofs
Install
Dune Dependency
Authors
Maintainers
Sources
zenon-0.7.1.tar.xz
md5=cb8b35e2d55dabcc7d8a1e8b3600f68a
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.
Published: 21 Nov 2013
On This Page