Satallax 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 Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year Satallax: an automatic higher-order prover. Zbl 1358.68250Brown, Chad E. 2012 Analytic tableaux for higher-order logic with choice. Zbl 1258.03019Backes, Julian; Brown, Chad Edward 2011 all top 5 Cited by 61 Authors 22 Benzmüller, Christoph Ewald 9 Blanchette, Jasmin Christian 9 Brown, Chad Edward 9 Urban, Josef 7 Kaliszyk, Cezary 7 Steen, Alexander 6 Bentkamp, Alexander 6 Woltzenlogel Paleo, Bruno 5 Paulson, Lawrence Charles 4 Vukmirović, Petar 4 Waldmann, Uwe 3 Bhayat, Ahmed 3 Cruanes, Simon 3 Reger, Giles 3 Sultana, Nik 3 Sutcliffe, Geoff 3 Tourret, Sophie 3 Wisniewski, Max 2 Backes, Julian 2 Böhme, Sascha 2 Färber, Michael 2 Gauthier, Thibault 2 Libal, Tomer 2 Miller, Dale Allen 2 Nummelin, Visa 2 Slaney, John K. 1 Barbosa, Haniel 1 Barrett, Clark W. 1 Berger, Ulrich 1 Chvalovský, Karel 1 Czajka, Łukasz 1 Defourné, Antoine 1 El Ouraoui, Daniel 1 Fleury, Mathias 1 Gabbay, Dov M. 1 Genovese, Valerio 1 Gleißner, Tobias 1 Hou, Tie 1 Irving, Geoffrey 1 Itegulov, Daniyar 1 Jakubův, Jan 1 Kaufmann, Matt 1 Kern, Kim 1 Kühlwein, Daniel 1 Loos, Sarah M. 1 L’vov, M. S. 1 Moore, J Strother 1 Peschanenko, V. S. 1 Raths, Thomas 1 Reynolds, Andrew 1 Rispoli, Daniele 1 Scott, Dana Stewart 1 Smolka, Steffen Juilf 1 Steckermeier, Albert 1 Suda, Martin 1 Szegedy, Christian 1 Tarasich, Yu. 1 Theiss, Frank 1 Tinelli, Cesare 1 Vyskočil, Jiří 1 Weber, Leon all top 5 Cited in 11 Serials 12 Journal of Automated Reasoning 3 Annals of Mathematics and Artificial Intelligence 2 Logical Methods in Computer Science 2 Journal of Formalized Reasoning 1 Journal of Philosophical Logic 1 AI Communications 1 MSCS. Mathematical Structures in Computer Science 1 Cybernetics and Systems Analysis 1 Logic and Logical Philosophy 1 Journal of Applied Logic 1 Logica Universalis Cited in 3 Fields 58 Computer science (68-XX) 33 Mathematical logic and foundations (03-XX) 1 Category theory; homological algebra (18-XX) Citations by Year