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)

There are some automated theorem provers
based on higher-order logic...
- Thomas Hales
Satallax Logo



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.
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.


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.


Gert Smolka: Satallax was 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.
Chris 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.