package zenon

  1. Overview
  2. Docs
An Extensible Automated Theorem Prover Producing Checkable Proofs

Install

Dune Dependency

Authors

Maintainers

Sources

0.8.4.tar.gz
sha256=1429c83323402ce0d2c18826f4a9abf9cfefb0f78ab72e56c451c6f4e344fae7
md5=c66dde20620b57d5b721a2ecb27cba25

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: 21 Sep 2018

Dependencies (1)

  1. ocaml >= "4.02.0" & < "5.0"

Dev Dependencies

None

Used by

None

Conflicts (2)

  1. coq-core
  2. coq >= "8.9"
OCaml

Innovation. Community. Security.