package zenon

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

Install

Dune Dependency

Authors

Maintainers

Sources

0.8.5.tar.gz
sha256=73811276ad0aa46e91e346bf38937d37b1b9930e0b9f6b0aa20a5c1959e3006e
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)

  1. ocaml >= "4.07.0"

Dev Dependencies

None

Used by

None

OCaml

Innovation. Community. Security.