package zenon_modulo

  1. Overview
  2. Docs
Zenon Modulo Theory

Install

Dune Dependency

Authors

Maintainers

Sources

0.5.0.tar.gz
md5=3e0a13775df0546b02d8d77d3834d777
sha512=9b70eddb40404011c4b593604c9974c3f81ffeac119ad190be3aa2964f98c60ee166aeff07eee62d51f26df9663e65eea4e181812ef0077892a421b50f1bc4f6

Description

Automated theorem prover for first order classical logic (with equality), based on the tableau method. Zenon_modulo handles first-order logic with equality. Its most important feature is that it outputs the proofs of the theorems, in Coq-checkable form.

Tags

automated theorem prover

Published: 26 Jan 2024

Dependencies (2)

  1. zarith >= "1.11"
  2. ocaml >= "4.08.0"

Dev Dependencies

None

Used by

None

OCaml

Innovation. Community. Security.