package zenon

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

Install

Dune Dependency

Authors

Maintainers

Sources

zenon-0.8.0.tar.gz
sha256=807d946af0295f54edd76ee5ec0563f85a307d7a6b313f98fe6942b32f80ec87
md5=4d82ae5b6dc498a73ef85a353c5da325

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: 10 Jun 2015

Dependencies (2)

  1. coq < "8.9"
  2. ocaml < "4.06.0"

Dev Dependencies

None

Used by

None

Conflicts

None

OCaml

Innovation. Community. Security.