Software Search - zbMATH Open

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

2 Publications describing the Software, including 2 Publications in zbMATH	Year
Satallax: an automatic higher-order prover. Zbl 1358.68250 Brown, Chad E.	2012
Analytic tableaux for higher-order logic with choice. Zbl 1258.03019 Backes, Julian; Brown, Chad Edward	2011

all top 5

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

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

58	Computer science (68-XX)
33	Mathematical logic and foundations (03-XX)
1	Category theory; homological algebra (18-XX)