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.

## News

**June, 2013:** Two versions of Satallax competed
in the

THF (higher-order) Division
of

CASC-24 and came in first and second.
Satallax-MaLeS 1.2 came in first solving 119 of 150 problems.
Satallax 2.7 (the latest "official" version available on this site) came in second solving solving 116 of 150 problems.

Satallax-MaLeS 1.2 is an alternative version of Satallax in which the strategy schedule
for was computed using machine learning techniques.

Daniel Kuehlwein is responsible for Satallax-MaLeS.

**July, 2012:** Satallax 2.4 came in second (or third) behind Isabelle 2012 (Sledgehammer)
in the

THF (higher-order) Division of

CASC-J6.
A demonstration system Isabelle-HOT 2012 which calls the higher-order provers Satallax and LEO (in addition to calling first-order systems and SMT solvers) was significantly better than all the other systems. Satallax 2.4 solved about 5% more problems than last year's winner, Satallax 2.1.

**February, 2011:** Satallax has been reimplemented in Objective Caml and released as Satallax 2.0.

**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 new system award.

## Downloads

The most recent version is below. All versions are available

here.

Satallax 2.7April 15, 2013

Starting with this version, Satallax can call the first-order theorem prover E during search.

Also, there are many new modes and a new strategy schedule.

## 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.