(Detailed Results)

(Detailed Results)

(Detailed Results)

(Detailed Results)

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.

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

Satallax 2.8July 2015

This version includes Nik Sultana's code to construct Isabelle proofs.

This version includes Nik Sultana's code to construct Isabelle proofs.

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.

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.

Satallax 2.6August 16, 2012

Fixed a bug with TPTP include directives that use full paths.

Fixed a bug with TPTP include directives that use full paths.

Satallax 2.5August 14, 2012

Added TSTP proof output.

Added TSTP proof output.

Satallax 2.4April 23, 2012

Added an implementation of higher-order preunification that is sometimes used to suggest instantiations.

Added support for demonstrating satisfiability in finite models.

Competed in CASC-J6

Added an implementation of higher-order preunification that is sometimes used to suggest instantiations.

Added support for demonstrating satisfiability in finite models.

Competed in CASC-J6

Satallax 2.3January 30, 2012

Upgraded to MiniSat 2.2.0.

Added code to lookup the value of propositional variables in the assignment. This can be used to guide the search.

Support for create Coq proof terms (for the simply typed fragment of Coq) has been added. This assumes Coq >= 8.4 (with eta conversion).

Upgraded to MiniSat 2.2.0.

Added code to lookup the value of propositional variables in the assignment. This can be used to guide the search.

Support for create Coq proof terms (for the simply typed fragment of Coq) has been added. This assumes Coq >= 8.4 (with eta conversion).

Satallax 2.2September 9, 2011

There is now an option for producing higher-order unsatisfiable cores.

The production of Coq proof scripts is more robust than in Satallax 2.1.

There is now an option for producing higher-order unsatisfiable cores.

The production of Coq proof scripts is more robust than in Satallax 2.1.

Satallax 2.1June 17, 2011

New flags and new modes have been added.

Support for producing Coq proof scripts has been added.

The code for producing proof scripts was written by Andreas Teucke.

Before producing proof scripts, PicoSAT is called to compute a minimal unsatisfiable core.

Competed in CASC-23; Winner of THF division

New flags and new modes have been added.

Support for producing Coq proof scripts has been added.

The code for producing proof scripts was written by Andreas Teucke.

Before producing proof scripts, PicoSAT is called to compute a minimal unsatisfiable core.

Competed in CASC-23; Winner of THF division

Satallax 2.0February 10, 2011

This is a complete reimplementation of Satallax in Objective Caml.

A foreign function interface is now used to interact with MiniSat code.

This is a complete reimplementation of Satallax in Objective Caml.

A foreign function interface is now used to interact with MiniSat code.

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.

This is the last version of Satallax coded in Lisp.

Competed in CASC-J5

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.

This is the last version of Satallax coded in Lisp.

Competed in CASC-J5

Satallax 1.2January 29, 2010

Shadowing is now disallowed. A name must be declared exactly once.

Shadowing is now disallowed. A name must be declared exactly once.

Satallax 1.1January 15, 2010

Satallax 1.0January 8, 2010

There are bugs when certain command line options are used in combination (-t with -m, -t with -M). (h/t Geoff Sutcliffe)

There are bugs when certain command line options are used in combination (-t with -m, -t with -M). (h/t Geoff Sutcliffe)

Satallax 2.8July 2015

This version includes Nik Sultana's code to construct Isabelle proofs.

This version includes Nik Sultana's code to construct Isabelle proofs.

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.