CLASSES=none
PSTAMP=q20151008200039
LICFILE=gpl2.txt
LICURL=http://www.gnu.org/licenses/gpl-2.0.html
LICINFO=GNU General Public License, Version 2, June 1991
DESC=Darwin is an automated theorem prover for first order clausal logic. It accepts problems formulated in tptp or tme format, non-clausal tptp problems are clausified using the eprover. Equality is not built into the currently implemented version of the calculus, it is instead automatically axiomatized for a given problem. Darwin is a decision procedure for function-free clause sets, and is in general faster and scales better on such problems than propositional approaches.
BASEDIR=/usr
VENDOR=LINOFEE, http://www.linofee.org
EMAIL=developers@linofee.org
CATEGORY=develop,application
NAME=Theorem Prover Darwin
SERIALNUM=001
VERSION=1.4.5
ARCH=i386
PKG=LNFdarwin