
People
Developers
Chad E. Brown: the primary developer.
He wrote most of the lisp code for Satallax 1.* and the search related ocaml code for Satallax 2.0.
Michael Färber wrote the Machine Learning code and did a major refactoring of the other code. His code is part of Satallax 3.0 (and above).
Nik Sultana wrote code to construct Isabelle proofs
from Satallax refutations.
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
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 of Chad Brown 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.