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 1 to 20 of 57.
Sorted by year (citations)

1 2 3 next

  1. Libal, Tomer; Miller, Dale: Functions-as-constructors higher-order unification: extended pattern unification (2022)
  2. Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe: Superposition for lambda-free higher-order logic (2021)
  3. Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2021)
  4. Defourné, Antoine: Improving automation for higher-order proof steps (2021)
  5. Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
  6. Vukmirović, Petar; Bentkamp, Alexander; Nummelin, Visa: Efficient full higher-order unification (2021)
  7. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  8. Kaufmann, Matt; Moore, J Strother: Limited second-order functionality in a first-order setting (2020)
  9. Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark: Extending SMT solvers to higher-order logic (2019)
  10. Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2019)
  11. Bhayat, Ahmed; Reger, Giles: Restricted combinatory unification (2019)
  12. Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
  13. Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for (\mathrmE) (2019)
  14. Bentkamp, Alexander; Blanchette, Jasmin Christian; Cruanes, Simon; Waldmann, Uwe: Superposition for (\lambda)-free higher-order logic (2018)
  15. Lvov, M.; Peschanenko, V.; Letychevskyi, O.; Tarasich, Y.; Baiev, A.: Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas (2018)
  16. Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
  17. Steen, Alexander; Benzmüller, Christoph: The higher-order prover Leo-III (2018)
  18. Benzmüller, Christoph: Cut-elimination for quantified conditional logic (2017)
  19. Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno: Computer-assisted analysis of the Anderson-Hájek ontological controversy (2017)
  20. Berger, Ulrich; Hou, Tie: A realizability interpretation of Church’s simple theory of types (2017)

1 2 3 next