eprover

E Theorem Prover
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.

Install
Published
21 Jan 2022
Sources
E.tgz
sha512=20ba97779b81b215296215e6fb10db742c16684c6a38a4612ee2c28a72917aaea8f87daea4cd49557f5b47720c62cffd38445cf779e6690dd0f0924d26b37683
Dependencies
Reverse Dependencies