package eprover

  1. Overview
  2. Docs
E Theorem Prover

Install

Dune Dependency

Authors

Maintainers

Sources

E.tgz
sha512=20ba97779b81b215296215e6fb10db742c16684c6a38a4612ee2c28a72917aaea8f87daea4cd49557f5b47720c62cffd38445cf779e6690dd0f0924d26b37683

Description

E is a theorem prover for full first-order logic with equality. It accepts a problem specification, typically consisting of a number of first-order clauses or formulas, and a conjecture, again either in clausal or full first-order form. The system will then try to find a formal proof for the conjecture, assuming the axioms.

Published: 21 Jan 2022

Dependencies (1)

  1. conf-gcc

Dev Dependencies

None

Used by

None

Conflicts

None