Satallax CASC-23 Trophy
CASC-23 THF Division Winner
(Detailed Results)

CASC-24 THF Division Runner Up/Winner
(Detailed Results)

CASC-J7 THF Division Runner Up/Winner
(Detailed Results)

CASC-25 THF Division Winner
(Detailed Results)

Satallax Logo

People

Developers

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). 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.
Andreas Teucke was a Bachelor student in Professor Gert Smolka's Lehrstuhl who wrote ocaml code to create Coq-readable proof terms 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

Geoff Sutcliffe: Geoff Sutcliffe runs the TPTP. He tests Satallax and makes sure it stays TPTP compliant. Satallax can be run online via the System On TPTP page.
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.
Niklas Eén and Niklas Sörensson are the authors of MiniSat, on top of which Satallax is built.
Daniel Kuehlwein is a researcher responsible for Satallax-MaLeS, an alternative version of Satallax with a strategy schedule computed using machine learning techniques.