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=jammy20220814064434
CLASSES=none