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
Documentation zenon-prover.org Edit opam file
Published
23 Oct 2020
Authors
Maintainers
Sources
0.8.5.tar.gz
md5=6c64d2c29bbcb3571f25f7f8c2dbea6c
Dependencies
ocaml >= "4.07.0"
Reverse Dependencies