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; Coq; z3; VAMPIRE; TPTP; Archive Formal Proofs; E Theorem Prover; HOL; Nitpick; HOL Light; Satallax; CVC4; SPASS; Flyspeck; Mizar; Isar; Metis_; SMT-LIB; seL4 Cited in: 157 Documents 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 203 Authors 28 Blanchette, Jasmin Christian 14 Guttmann, Walter 12 Benzmüller, Christoph Ewald 10 Kaliszyk, Cezary 10 Urban, Josef 9 Paulson, Lawrence Charles 9 Reynolds, Andrew 7 Bentkamp, Alexander 7 Foster, Simon 7 Popescu, Andrei 7 Tinelli, Cesare 6 Barrett, Clark W. 6 Böhme, Sascha 5 Fleury, Mathias 5 Nipkow, Tobias 5 Sutcliffe, Geoff 5 Tourret, Sophie 5 Vukmirović, Petar 5 Weidenbach, Christoph 4 Avigad, Jeremy 4 Berghammer, Rudolf 4 Cruanes, Simon 4 Kühlwein, Daniel 4 Reger, Giles 4 Struth, Georg 4 Woodcock, James C. P. 3 Barbosa, Haniel 3 Brown, Chad Edward 3 Färber, Michael 3 Höfner, Peter 3 Janičić, Predrag 3 Narboux, Julien 3 Niemetz, Aina 3 Preiner, Mathias 3 Scott, Dana Stewart 3 Traytel, Dmitry 3 Waldmann, Uwe 3 Wenzel, Makarius 3 Woltzenlogel Paleo, Bruno 3 Zeyda, Frank 3 Zohar, Yoni 2 Alama, Jesse 2 Armstrong, Alasdair 2 Berger, Ulrich 2 Bhayat, Ahmed 2 Bourke, Timothy 2 Bundy, Alan 2 Cavalcanti, Ana 2 Desharnais, Martin 2 Dubut, Jérémy 2 Fleuriot, Jacques D. 2 Fuenmayor, David 2 Grov, Gudmund 2 Johansson, Moa 2 Klein, Gerwin 2 Korovin, Konstantin 2 Lawrence, Andrew 2 Leino, K. Rustan M. 2 Lewis, Robert Y. 2 Nagashima, Yutaka 2 Nummelin, Visa 2 Parent, Xavier 2 Pease, Alison 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 van der Torre, Leendert W. N. 2 Villadsen, Jørgen 2 Viswanathan, Arjun 2 Voronkov, Andrei 2 Weber, Tjark 2 Yamada, Akihisa 1 Åman Pohjola, Johannes 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 Cristiá, Maximiliano 1 Dalvandi, Sadegh 1 Daum, Matthias 1 De Luca, Guido 1 Doherty, Simon 1 Dongol, Brijesh 1 Dragoste, Irina 1 Einarsdóttir, Sólrún Halla ...and 103 more Authors all top 5 Cited in 19 Serials 35 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 19 Fields 151 Computer science (68-XX) 50 Mathematical logic and foundations (03-XX) 5 Combinatorics (05-XX) 3 Category theory; homological algebra (18-XX) 2 General and overarching topics; collections (00-XX) 2 General algebraic systems (08-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 Group theory and generalizations (20-XX) 1 Real functions (26-XX) 1 Geometry (51-XX) 1 Probability theory and stochastic processes (60-XX) 1 Relativity and gravitational theory (83-XX) 1 Geophysics (86-XX) 1 Systems theory; control (93-XX) 1 Mathematics education (97-XX) Citations by Year