CLASSES=none
PSTAMP=q20151027041345
LICFILE=mpi.txt
LICURL=http://www.spass-prover.org/
LICINFO=MPI BSD style license
DESC=SPASS is an automated theorem prover for first-order logic with equality. So the input for the prover is a first-order formula in our syntax. Running SPASS on such a formula results in the final output SPASS beiseite: Proof found. if the formula is valid, SPASS beiseite: Completion found. if the formula is not valid and because validity in first-order logic is undecidable, SPASS may run forever without producing any final result.
BASEDIR=/usr
VENDOR=LINOFEE, http://www.linofee.org
EMAIL=developers@linofee.org
CATEGORY=develop,application
NAME=Theorem Prover SPASS
SERIALNUM=001
VERSION=3.7
ARCH=i386
PKG=LNFspass