Satallax CASC-23 Trophy
CASC-23 THF Division Winner
(Detailed Results)

CASC-24 THF Division Runner Up/Winner
(Detailed Results)

CASC-J7 THF Division Runner Up/Winner
(Detailed Results)

CASC-25 THF Division Winner
(Detailed Results)

Satallax Logo
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 Objective Caml. You can run Satallax online at the System On TPTP website.

Satallax is no longer being maintained or developed. It is open source so everyone should feel free to maintain or develop it themselves. The last released version (3.4) does not compile in some circumstances. Here is a slightly updated version: Satallax 3.4b.

Versions of Satallax from circa 2016 until circa 2021 were developed and maintained by Michael Färber. For more information see Michael Färber's Satallax page.

There is also a fork of Satallax called Lash that gives fast efficient implementations of vital structures and operations in C.

Downloads

The most recent version is below. All versions are available here.

Satallax 3.4b

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.