has been the primary developer of Satallax since Version 3.0.
Färber's work on Satallax has supported by Cezary Kaliszyk and Josef Urban.
wrote code to construct Isabelle proofs
from Satallax refutations.
: the first developer.
He wrote most of the lisp code for Satallax 1.* and the search related ocaml code for Satallax 2.0.
: Frank Theiß wrote ocaml code to parse TPTP syntax. This code
was written to be used in LEO-II, but it has now also been used in Satallax.
Since 2015 Satallax is developed with the support of Josef Urban's
Automated Reasoning Group
at Czech Technical University in Prague.
Urban's group was already responsible for developing
the machine learning variant Satallax-MaLeS earlier (see Daniel Kuehlwein below).
Since moving to Prague, Satallax has incorporated premise selection (including
some machine learning techniques) and support for Mizar-like soft typing.
The group of Cezary Kaliszyk at University of Innsbruck
has also supported development of Satallax, through support
of Michael Färber as well as productive discussions with Kaliszyk and other members of his group.
Satallax was initially developed in Gert Smolka's Lehrstuhl
Universität des Saarlandes
The search procedure for Satallax is largely based on a complete tableau calculus
for simple type theory without choice developed by
Brown and Smolka
The results on restricted instantiations which permit Satallax to terminate indicating
satisfiability in some essentially first-order problems
also come from the work of Brown and Smolka.
Julian Backes was a Master student in the Smolka Lehrstuhl.
Backes and Brown extended the tableau calculus of Brown and Smolka to be complete
for simple type theory with a
is the primary developer of LEO-II
and has done a lot of work in higher-order theorem proving for a long time.
Satallax and LEO-II use some of the same parsing code.
is a researcher responsible for Satallax-MaLeS
an alternative version of Satallax with a strategy schedule computed using machine learning techniques.