PKG=LNFspass ARCH=x86_64 VERSION=3.9 SERIALNUM=001 NAME=Theorem Prover SPASS CATEGORY=develop,application EMAIL=jel+ubuntu-pkg@cs.uni-magdeburg.de VENDOR=http://theo.iks.cs.ovgu.de/ BASEDIR=/usr 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. LICINFO=MPI BSD style license LICURL=http://www.spass-prover.org/ LICFILE=mpi.txt PSTAMP=xenial20180510070326 CLASSES=none