SPASS swMATH ID: 4108 Software Authors: C Weidenbach, U Brahm, T Hillenbrand Description: SPASS is an automated theorem prover for first-order logic with equality. So the input for the prover is a first-order formula in our syntax. Running SPASS on such a formula results in the final output SPASS beiseite: Proof found. if the formula is valid, SPASS beiseite: Completion found. if the formula is not valid and because validity in first-order logic is undecidable, SPASS may run forever without producing any final result. Homepage: http://www.spass-prover.org/ Related Software: VAMPIRE; TPTP; E Theorem Prover; Isabelle/HOL; OTTER; z3; Sledgehammer; Mace4; iProver; Mizar; Isabelle; Coq; SETHEO; Waldmeister; CVC4; FLOTTER; HOL; SATCHMO; Bliksem; Prover9 Cited in: 192 Publications Further Publications: http://www.spass-prover.org/publications.html Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year SPASS version 2.0. Zbl 1072.68596Weidenbach, Christoph; Brahm, Uwe; Hillenbrand, Thomas; Keen, Enno; Theobald, Christian; Topić, Dalibor 2002 all top 5 Cited by 248 Authors 21 Weidenbach, Christoph 14 Hustadt, Ullrich 12 Schmidt, Renate A. 10 Urban, Josef 9 Benzmüller, Christoph Ewald 9 Sutcliffe, Geoff 8 Meier, Andreas 7 Baumgartner, Peter 7 Blanchette, Jasmin Christian 7 de Nivelle, Hans 7 Dixon, Clare 7 Sorge, Volker 7 Waldmann, Uwe 6 Voronkov, Andrei 5 Bonacina, Maria Paola 5 Hillenbrand, Thomas 5 Schulz, Stephan 4 Colton, Simon 4 Kaliszyk, Cezary 4 Kovács, Laura Ildikó 4 McCasland, Roy L. 4 Nalon, Cláudia 4 Paulson, Lawrence Charles 4 Plaisted, David Alan 4 Siekmann, Jörg H. 4 Zhang, Lan 3 Areces, Carlos 3 Böhme, Sascha 3 Bromberger, Martin 3 Claessen, Koen 3 Cruanes, Simon 3 Fietzke, Arnaud 3 Fleury, Mathias 3 Giunchiglia, Enrico 3 Korovin, Konstantin 3 Lyaletski, Alexander V. 3 Paskevich, Andrei 3 Peltier, Nicolas 3 Suda, Martin 3 Tacchella, Armando 3 Theiss, Frank 3 Tinelli, Cesare 3 Verchinine, Konstantin 2 Bentkamp, Alexander 2 Brown, Chad Edward 2 Burel, Guillaume 2 Chaudhari, Dipak L. 2 Damani, Om P. 2 Davis, Ernest 2 de Rijke, Maarten 2 Duarte, André 2 Echenim, Mnacho 2 Fischer, Bernd 2 Fuchs, Dirk 2 Gorín, Daniel 2 Goubault-Larrecq, Jean 2 Höfner, Peter 2 Janičić, Predrag 2 Kapur, Deepak 2 Kruglov, Evgeniĭ Valentinovich 2 Lillieström, Ann 2 Ludwig, Michel 2 Melis, Erica 2 Moser, Georg 2 Narboux, Julien 2 Nipkow, Tobias 2 Papacchini, Fabio 2 Roggenbach, Markus 2 Schlichtkrull, Anders 2 Schumann, Johann M. Ph. 2 Sofronie-Stokkermans, Viorica 2 Steel, Graham 2 Stojanović Đurđević, Sana 2 Tishkovsky, Dmitry 2 Topić, Dalibor 2 Tourret, Sophie 2 Tran, Duc-Khanh 2 van der Torre, Leendert W. N. 2 Woltzenlogel Paleo, Bruno 1 Afshordel, Bijan 1 Alama, Jesse 1 Armando, Alessandro 1 Autexier, Serge 1 Azmy, Noran 1 Bancerek, Grzegorz 1 Barbosa, Haniel 1 Barrett, Clark W. 1 Bensalem, Saddek 1 Berghammer, Rudolf 1 Blohm, Antje 1 Bos, Johan 1 Brahm, Uwe 1 Bridge, James P. 1 Buchberger, Bruno 1 Bundy, Alan 1 Cerna, David M. 1 Cialdea Mayer, Marta 1 Crǎciun, Adrian 1 Dahn, Bernd Ingo 1 de Lima, Tiago ...and 148 more Authors all top 5 Cited in 24 Serials 32 Journal of Automated Reasoning 8 Annals of Mathematics and Artificial Intelligence 5 Artificial Intelligence 5 Journal of Symbolic Computation 4 ACM Transactions on Computational Logic 3 Journal of Applied Logic 2 AI Communications 2 Journal of Applied Non-Classical Logics 2 Mathematics in Computer Science 1 Commentationes Mathematicae Universitatis Carolinae 1 Science of Computer Programming 1 Annals of Pure and Applied Logic 1 Information and Computation 1 Formal Aspects of Computing 1 Journal of Logic and Computation 1 MSCS. Mathematical Structures in Computer Science 1 The Journal of Artificial Intelligence Research (JAIR) 1 Logic Journal of the IGPL 1 Fundamenta Informaticae 1 Computational Linguistics 1 Lecture Notes in Computer Science 1 Logica Universalis 1 Journal of Formalized Reasoning 1 Journal of Logical and Algebraic Methods in Programming all top 5 Cited in 11 Fields 176 Computer science (68-XX) 83 Mathematical logic and foundations (03-XX) 3 Group theory and generalizations (20-XX) 3 Information and communication theory, circuits (94-XX) 2 General and overarching topics; collections (00-XX) 2 Order, lattices, ordered algebraic structures (06-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 History and biography (01-XX) 1 General algebraic systems (08-XX) 1 Commutative algebra (13-XX) 1 Category theory; homological algebra (18-XX) Citations by Year