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.
Satallax is implemented in
Steel Bank Common Lisp.
You can run Satallax online at the
System On TPTP website.
News
July, 2010: Satallax 1.4 came in second in the higher-order THF division of
CASC-J5. (Click
here for results
and
here for detailed results.)
Satallax won the best newcomer award.
Downloads
The most recent version is below. All versions are available
here.
Satallax 1.4June 2, 2010
A number of extensions to the search procedure have been implemented. New modes that use these extensions have been added.
The strategy has been adjusted to use some of the new modes.
Extension 1. A preprocessing phase has been added. This splits a problem into independent problems if possible.
Extension 2. Subterms of the original problem can be preemptively used as instantiations.
Extension 3. Some modes use higher-order clauses and pattern matching during search.
Finally, bug in pattern matching from version 1.3 has been fixed.
Brief Description
Satallax progressively generates higher-order formulas and corresponding
propositional clauses. These formulas and propositional clauses correspond to a
complete tableau calculus for higher-order logic with a choice operator.
Satallax uses the SAT solver
MiniSat as an engine to test the current set of propositional clauses
for unsatisfiability.
If the clauses are unsatisfiable, then the original set of higher-order formulas is unsatisfiable.
If there are no quantifiers at function types, the generation of higher-order formulas
and corresponding clauses may terminate. In such a case, if MiniSat reports the final
set of clauses as satisfiable, then the original set of higher-order formulas is satisfiable.
The theorem prover Satallax is spelled Satallax, as opposed to any of the following:
Satellax, Satillax, Satalax, Sattalax, Satelax, Sattilax,
and so on. This footnote is included to help search engines.