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
10 Jun 2015
Authors
Maintainers
Sources
zenon-0.8.0.tar.gz
md5=4d82ae5b6dc498a73ef85a353c5da325
Dependencies
coq < "8.9"
ocaml < "4.06.0"
Reverse Dependencies