People
Developers
Michael Färber 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.
Nik Sultana wrote code to construct Isabelle proofs
from Satallax refutations.
Roj Blake: the first developer.
He wrote most of the lisp code for Satallax 1.* and the search related ocaml code for Satallax 2.0.
Contributors
Frank Theiß: 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.
Acknowledgements
Josef Urban:
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.
Cezary Kaliszyk
:
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.
Gert Smolka:
Satallax was initially developed in Gert Smolka's
Lehrstuhl at
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:
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
choice operator.
Christoph Benzmüller
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.
Daniel Kuehlwein
is a researcher responsible for
Satallax-MaLeS,
an alternative version of Satallax with a strategy schedule computed using machine learning techniques.