swMATH ID: 6849
Software Authors: Chad E. Brown; Andreas Teucke; Geoff Sutcliffe; Frank Theiß; Gert Smolka; Julian Backes; Chris Benzmüller
Description: Satallax is an automated theorem prover for higher-order logic. The particular form of higher-order logic supported by Satallax is Church’s simple type theory with extensionality and choice operators. The SAT solver MiniSat is responsible for much of the search for a proof. Satallax generates propositional clauses corresponding to rules of a complete tableau calculus and calls MiniSat periodically to test satisfiability of these clauses. Satallax is implemented in Objective Caml. You can run Satallax online at the System On TPTP website.
Homepage: http://www.ps.uni-saarland.de/~cebrown/satallax/
Keywords: higher-order logic; tableau calculus; simple type theory with choice; automated theorem proving; axiom of choice; Henkin models; higher-order automated theorem-prover { t Satallax}
Related Software: TPTP; Isabelle/HOL; LEO-II; E Theorem Prover; VAMPIRE; Sledgehammer; HOL; TPS; Coq; Leo-III; HOL Light; Nitpick; SPASS; CVC4; Flyspeck; Mizar; ML; StarExec; Metis_; MiniSat
Cited in: 62 Publications

Citations by Year