PKG=LNFeprover ARCH=x86_64 VERSION=2.5 SERIALNUM=001 NAME=Theorem Prover E CATEGORY=develop,application EMAIL=jel+ubuntu-pkg@cs.uni-magdeburg.de VENDOR=http://theo.iks.cs.ovgu.de/ BASEDIR=/usr 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). LICINFO=GNU General Public License, Version 2, June 1991 LICURL=http://www.gnu.org/licenses/gpl-2.0.html LICFILE=gpl2.txt PSTAMP=focal20201027193953 CLASSES=none