CLASSES=none
PSTAMP=q20151205213230
LICFILE=mit.txt
LICURL=http://www.opensource.org/licenses/mit-license.html
LICINFO=MIT License (free)
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.
BASEDIR=/usr
VENDOR=LINOFEE, http://www.linofee.org
EMAIL=developers@linofee.org
CATEGORY=develop,application
NAME=Theorem Prover Satallax
SERIALNUM=001
VERSION=2.7
ARCH=i386
PKG=LNFsatallax