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
-
23 Oct 2020
- Authors
-
- Maintainers
-
Sources
Dependencies
ocaml
>= "4.07.0"
Reverse Dependencies