Sledgehammer swMATH ID: 7047 Software Authors: Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C. Description: Sledgehammer is a tool that harnesses external first-order automatic theorem provers (ATPs) to discharge interactive proof obligations arising in Isabelle/HOL. We extended it with LEO-II and Satallax, the two most prominent higher-order ATPs, improving its performance on higher-order problems. To explore their usefulness, these ATPs are measured against first-order ATPs and built-in Isabelle tactics on a variety of benchmarks from Isabelle and the TPTP library. Sledgehammer provides an ideal test bench for individual features of LEO-II and Satallax, revealing areas for improvements. Homepage: http://isabelle.in.tum.de/website-Isabelle2009-1/sledgehammer.html Keywords: higher-order logic; automatic theorem provers; proof assistants Related Software: Isabelle/HOL; Isabelle; z3; Coq; VAMPIRE; Archive Formal Proofs; E Theorem Prover; TPTP; Nitpick; HOL; HOL Light; Mizar; Flyspeck; Satallax; Metis_; SPASS; Isar; CVC4; SMT-LIB; seL4 Cited in: 144 Publications Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year LEO-II and Satallax on the Sledgehammer test bench. Zbl 1262.68161Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C. 2013 Extending Sledgehammer with SMT solvers. Zbl 1314.68271Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. 2011 all top 5 Cited by 183 Authors 25 Blanchette, Jasmin Christian 13 Guttmann, Walter 12 Benzmüller, Christoph Ewald 10 Kaliszyk, Cezary 10 Urban, Josef 9 Paulson, Lawrence Charles 8 Reynolds, Andrew 7 Foster, Simon 7 Popescu, Andrei 6 Böhme, Sascha 6 Tinelli, Cesare 5 Barrett, Clark W. 5 Fleury, Mathias 5 Nipkow, Tobias 5 Sutcliffe, Geoff 5 Weidenbach, Christoph 4 Avigad, Jeremy 4 Bentkamp, Alexander 4 Berghammer, Rudolf 4 Kühlwein, Daniel 4 Reger, Giles 4 Struth, Georg 4 Woodcock, James C. P. 3 Brown, Chad Edward 3 Färber, Michael 3 Höfner, Peter 3 Scott, Dana Stewart 3 Traytel, Dmitry 3 Waldmann, Uwe 3 Wenzel, Makarius 3 Woltzenlogel Paleo, Bruno 3 Zeyda, Frank 2 Alama, Jesse 2 Armstrong, Alasdair 2 Barbosa, Haniel 2 Berger, Ulrich 2 Bhayat, Ahmed 2 Bourke, Timothy 2 Bundy, Alan 2 Cavalcanti, Ana 2 Cruanes, Simon 2 Desharnais, Martin 2 Fuenmayor, David 2 Grov, Gudmund 2 Janičić, Predrag 2 Klein, Gerwin 2 Korovin, Konstantin 2 Lawrence, Andrew 2 Leino, K. Rustan M. 2 Lewis, Robert Y. 2 Narboux, Julien 2 Niemetz, Aina 2 Parent, Xavier 2 Pease, Alison 2 Preiner, Mathias 2 Raggi, Daniel 2 Roux, Cody 2 Schlichtkrull, Anders 2 Seisenberger, Monika 2 Smallbone, Nicholas 2 Steen, Alexander 2 Sternagel, Christian 2 Stojanović Đurđević, Sana 2 Sultana, Nik 2 Tourret, Sophie 2 van der Torre, Leendert W. N. 2 Villadsen, Jørgen 2 Voronkov, Andrei 2 Vukmirović, Petar 2 Weber, Tjark 2 Zohar, Yoni 1 Back, Ralph-Johan 1 Barendregt, Hendrik Pieter 1 Bauereiß, Thomas 1 Beeson, Michael J. 1 Benda, Miroslav 1 Bezem, Marc 1 Bonacina, Maria Paola 1 Boulmé, Sylvain 1 Bromberger, Martin 1 Bulwahn, Lukas 1 Canham, Samuel 1 Cheney, James 1 Claessen, Koen 1 Dalvandi, Sadegh 1 Daum, Matthias 1 Doherty, Simon 1 Dongol, Brijesh 1 Dragoste, Irina 1 Dubut, Jérémy 1 El Ouraoui, Daniel 1 Eriksson, Johannes 1 Eschen, Agnes Moesgård 1 Faqeh, Rasha 1 Fetzer, Christof 1 Filliâtre, Jean-Christophe 1 Fox, Anthony C. J. 1 Freitas, Leo 1 From, Asta Halkjær 1 Furusawa, Hitoshi ...and 83 more Authors all top 5 Cited in 19 Serials 30 Journal of Automated Reasoning 7 Journal of Logical and Algebraic Methods in Programming 4 Logical Methods in Computer Science 3 Formal Aspects of Computing 3 AI Communications 2 Theoretical Computer Science 2 Annals of Mathematics and Artificial Intelligence 2 Theory and Practice of Logic Programming 2 Mathematics in Computer Science 1 Acta Informatica 1 Artificial Intelligence 1 Bulletin of the Section of Logic 1 Journal of Symbolic Computation 1 Journal of Logic, Language and Information 1 Advances in Applied Clifford Algebras 1 The Journal of Logic and Algebraic Programming 1 Journal of Applied Logic 1 Journal of Formalized Reasoning 1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences all top 5 Cited in 16 Fields 138 Computer science (68-XX) 45 Mathematical logic and foundations (03-XX) 5 Combinatorics (05-XX) 2 General and overarching topics; collections (00-XX) 2 General algebraic systems (08-XX) 2 Category theory; homological algebra (18-XX) 1 History and biography (01-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Number theory (11-XX) 1 Field theory and polynomials (12-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Real functions (26-XX) 1 Geometry (51-XX) 1 Probability theory and stochastic processes (60-XX) 1 Systems theory; control (93-XX) 1 Mathematics education (97-XX) Citations by Year