eproverversion

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.

AuthorsStephan Schulz, Simon Cruanes, Petar Vukmirovic, Mohamed Bassem and Martin Moehrmann
LicenseLGPL-2.1-or-later OR GPL-2.0-or-later
Published
Homepagehttps://www.eprover.org
Issue TrackerStephan Schulz (see homepage for email)
Maintainer7895506+MSoegtropIMC@users.noreply.github.com
Dependencies
Source [http] http://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_3.0/E.tgz
sha512=a4d90080c400579beb0a1b43ffbcb6d9b1435abb72807b1a51acd6311f975f37204368bdfee1a1c15ea46111cbe7497f9b25a5bf2eed6032b8d47e29455c31e3
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/eprover/eprover.3.0/opam
No package is dependent