PKG=LNFsatallax
ARCH=x86_64
VERSION=2.7
SERIALNUM=001
NAME=Theorem Prover Satallax
CATEGORY=develop,application
EMAIL=jel+ubuntu-pkg@cs.uni-magdeburg.de
VENDOR=http://theo.iks.cs.ovgu.de/
BASEDIR=/usr
DESC=Satallax is an automated theorem prover for higher-order logic. The particular form of higher-order logic supported by Satallax is Church's simple type theory with extensionality and choice operators. The SAT solver MiniSat is responsible for much of the search for a proof. Satallax generates propositional clauses corresponding to rules of a complete tableau calculus and calls MiniSat periodically to test satisfiability of these clauses. The bundled version of picosat and picomus have been renamed to picosat4satallax and picomus4satallax repectively to avoid name clashes with more recent versions of picosat.
LICINFO=MIT License (free)
LICURL=http://www.opensource.org/licenses/mit-license.html
LICFILE=mit.txt
PSTAMP=focal20201029120702
CLASSES=none