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 55 articles , 2 standard articles )

Showing results 21 to 40 of 55.
Sorted by year (citations)
  1. Gleißner, Tobias; Steen, Alexander; Benzmüller, Christoph: Theorem provers for every normal modal logic (2017)
  2. Itegulov, Daniyar; Slaney, John; Woltzenlogel Paleo, Bruno: Scavenger 0.1: a theorem prover based on conflict resolution (2017)
  3. Loos, Sarah; Irving, Geoffrey; Szegedy, Christian; Kaliszyk, Cezary: Deep network guided proof search (2017)
  4. Sutcliffe, Geoff: The CADE-26 automated theorem proving system competition -- CASC-26 (2017)
  5. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  6. Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef: Hammering towards QED (2016)
  7. Brown, Chad E.; Urban, Josef: Extracting higher-order goals from the Mizar Mathematical Library (2016)
  8. Färber, Michael; Brown, Chad: Internal guidance for Satallax (2016)
  9. Libal, Tomer; Miller, Dale: Functions-as-constructors higher-order unification (2016)
  10. Steen, Alexander; Benzmüller, Christoph: Sweet SIXTEEN: automation via embedding into classical higher-order logic (2016)
  11. Steen, Alexander; Wisniewski, Max; Benzmüller, Christoph: Agent-based HOL reasoning (2016)
  12. Wisniewski, Max; Steen, Alexander; Kern, Kim; Benzmüller, Christoph: Effective normalization techniques for HOL (2016)
  13. Benzmüller, Christoph: Higher-order automated theorem provers (2015)
  14. Benzmüller, Christoph: Invited talk: On a (quite) universal theorem proving approach and its application in metaphysics (2015)
  15. Benzmüller, Christoph; Paleo, Bruno Woltzenlogel: Interacting with modal logics in the Coq proof assistant (2015)
  16. Benzmüller, Christoph; Paleo, Bruno Woltzenlogel: On logic embeddings and Gödel’s God (2015)
  17. Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover \textscLeo-II (2015)
  18. Kühlwein, Daniel; Urban, Josef: MaLeS: a framework for automatic tuning of automated theorem provers (2015)
  19. Sultana, Nik; Benzmüller, Christoph; Paulson, Lawrence C.: Proofs and reconstructions (2015)
  20. Wisniewski, Max; Steen, Alexander; Benzmüller, Christoph: \textscLeoPARD-- a generic platform for the implementation of higher-order reasoners (2015)