Satallax

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.


References in zbMATH (referenced in 57 articles , 2 standard articles )

Showing results 41 to 57 of 57.
Sorted by year (citations)
  1. Sultana, Nik; Benzmüller, Christoph; Paulson, Lawrence C.: Proofs and reconstructions (2015)
  2. Wisniewski, Max; Steen, Alexander; Benzmüller, Christoph: \textscLeoPARD-- a generic platform for the implementation of higher-order reasoners (2015)
  3. Benzmüller, Christoph; Woltzenlogel Paleo, Bruno: Automating Gödel’s ontological proof of God’s existence with higher-order automated theorem provers (2014)
  4. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with (\mathsfFlyspeck) (2014)
  5. Benzmüller, Christoph; Raths, Thomas: HOL based first-order modal logic provers (2013)
  6. Brown, Chad E.: Reducing higher-order theorem proving to a sequence of SAT problems (2013)
  7. Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C.: LEO-II and Satallax on the Sledgehammer test bench (2013)
  8. Urban, Josef; Vyskočil, Jiří: Theorem proving in large formal mathematics as an emerging AI field (2013)
  9. Benzmüller, Christoph; Gabbay, Dov; Genovese, Valerio; Rispoli, Daniele: Embedding and automating conditional logics in classical higher-order logic (2012)
  10. Brown, Chad E.: Satallax: an automatic higher-order prover (2012)
  11. Backes, Julian; Brown, Chad Edward: Analytic tableaux for higher-order logic with choice (2011)
  12. Benzmüller, Christoph: Combining and automating classical and non-classical logics in classical higher-order logics (2011)
  13. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2011)
  14. Brown, Chad E.: Reducing higher-order theorem proving to a sequence of SAT problems (2011)
  15. Backes, Julian; Brown, Chad E.: Analytic tableaux for higher-order logic with choice (2010)
  16. Benzmüller, Christoph: Verifying the modal logic cube is an easy task (for higher-order automated reasoners) (2010)
  17. Sutcliffe, Geoff; Benzmüller, Christoph: Automated reasoning in higher-order logic using the TPTP THF infrastructure (2010)