CLASSES=none
PSTAMP=q20170901211341
LICFILE=gpl2.txt
LICURL=http://www.gnu.org/licenses/gpl-2.0.html
LICINFO=GNU General Public License, Version 2, June 1991
DESC=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. If a proof is found, the system can provide a detailed list of proof steps that can be individually verified. If the conjecture is existential (i.e. it is of the form 'there exists an X with property P'), the latest versions can also provide possible answers (values for X).
BASEDIR=/usr
VENDOR=LINOFEE, http://www.linofee.org
EMAIL=developers@linofee.org
CATEGORY=develop,application
NAME=Theorem Prover E
SERIALNUM=001
VERSION=2.0
ARCH=i386
PKG=LNFeprover