package zenon
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
An Extensible Automated Theorem Prover Producing Checkable Proofs
Install
Authors
Maintainers
Sources
0.8.5.tar.gz
md5=6c64d2c29bbcb3571f25f7f8c2dbea6c
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: 23 Oct 2020
Dependencies (1)
-
ocaml
>= "4.07.0"
Dev Dependencies
Used by
Conflicts (3)
- ocaml-option-bytecode-only
- coq-core
-
coq
< "8.6"
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page