eproverversion Documentation on ocaml.org
E Theorem Prover
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.
| Authors | Stephan Schulz, Simon Cruanes, Petar Vukmirovic, Mohamed Bassem and Martin Moehrmann |
|---|---|
| Licenses | LGPL-2.1-or-later and GPL-2.0-or-later |
| Published | |
| Homepage | https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html |
| Issue Tracker | Stephan Schulz (see homepage for email) |
| Maintainer | 7895506+MSoegtropIMC@users.noreply.github.com |
| Dependencies | |
| Source [http] | http://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_2.6/E.tgz sha512=20ba97779b81b215296215e6fb10db742c16684c6a38a4612ee2c28a72917aaea8f87daea4cd49557f5b47720c62cffd38445cf779e6690dd0f0924d26b37683 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/eprover/eprover.2.6/opam |
No package is dependent
