Downloads
Below are releases in reverse chronological order.
Satallax 3.3February 2018
Satallax 3.3 adds support for Mizar style soft typing.
Satallax 3.2May 2017
Satallax 3.2 fixes a bug that previously caused Satallax to report failure if one of the slaves in the strategy schedule reported a bug.
Satallax 3.1March 2017
A premise selection algorithm based on SInE has been added. It is activated only if the problem is sufficiently big.
The proof construction for TSTP style proofs has been rewritten to do something faster and simpler.
Satallax 3.0June 2016
Michael Färber did some major refactoring of the code, and also included some machine learning code.
There is now the option of using interpretations to help choose instantiations.
Proof reconstruction can now be done even when E is called.
Satallax 2.8July 2015
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.
Satallax 2.6August 16, 2012
Fixed a bug with TPTP include directives that use full paths.
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
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).
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.
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
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.
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
Satallax 1.2January 29, 2010
Shadowing is now disallowed. A name must be declared exactly once.
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)
