eproverversion Documentation on ocaml.org
E Theorem Prover
E is a theorem prover for first-order and higher-order logic with equality. It accepts a problem specification, typically consisting of a number of first-order clauses or formulas, and a conjecture, in clausal or full first-order/higher-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 |
|---|---|
| License | LGPL-2.1-or-later OR GPL-2.0-or-later |
| Published | |
| Homepage | https://www.eprover.org |
| 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_3.0/E.tgz sha512=a4d90080c400579beb0a1b43ffbcb6d9b1435abb72807b1a51acd6311f975f37204368bdfee1a1c15ea46111cbe7497f9b25a5bf2eed6032b8d47e29455c31e3 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/eprover/eprover.3.0/opam |
No package is dependent
