• en

zenon

Automated theorem prover for first order classical logic (with equality), based on the tableau method

Zenon is an automatic theorem prover written in OCaml. Zenon handles first-order logic with equality. Its most important feature is that it outputs the proofs of the theorems, in Coq-checkable form.

Maintainer contact@ocamlpro.com

Events

Aug 21, 2012

Published version 0.7.1