Introduction
Satallax is an automated theorem prover for higher-order logic. It was initiated by Chad Brown.
My original connection with Satallax was its extension with internal guidance, which made Satallax learn from previous proof attempts, thus guiding the search to find more proofs in the future.
I took over the development of Satallax in 2018.
Downloads
- Satallax 3.4 (winner of CASC-27’s THF division)
This version makes use of E’s support for lambda-free higher-order logic developed by Petar Vukmirović. Further additions include an updated parser, a more deterministic proof search (limiting the number of E’s inference steps instead of its runtime), and improvements to SInE. Support for internal guidance and Mizar typing has been removed.
IJCAR 2016
To reproduce our results for IJCAR 2016, download all the files below, then look at the instructions in the evaluation tool package.