zenon

An 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.

Install
Published
21 Sep 2018
Authors
Maintainers
Sources
0.8.4.tar.gz
md5=c66dde20620b57d5b721a2ecb27cba25
Dependencies
ocaml >= "4.02.0" & < "5.0"
Reverse Dependencies
Conflicts
coq >= "8.9"