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; Archive Formal Proofs; z3; VAMPIRE; TPTP; E Theorem Prover; Nitpick; HOL; HOL Light; CVC4; Satallax; Mizar; Isar; SPASS; Flyspeck; Metis_; SMT-LIB; seL4 Cited in: 175 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 222 Authors 29 Blanchette, Jasmin Christian 15 Guttmann, Walter 14 Benzmüller, Christoph Ewald 10 Kaliszyk, Cezary 10 Urban, Josef 9 Paulson, Lawrence Charles 9 Reynolds, Andrew 8 Tinelli, Cesare 7 Barrett, Clark W. 7 Bentkamp, Alexander 7 Foster, Simon 7 Popescu, Andrei 6 Böhme, Sascha 6 Sutcliffe, Geoff 6 Vukmirović, Petar 6 Weidenbach, Christoph 5 Fleury, Mathias 5 Nipkow, Tobias 5 Tourret, Sophie 4 Avigad, Jeremy 4 Barbosa, Haniel 4 Berghammer, Rudolf 4 Cruanes, Simon 4 Desharnais, Martin 4 Kühlwein, Daniel 4 Reger, Giles 4 Struth, Georg 4 Woodcock, James C. P. 4 Zohar, Yoni 3 Brown, Chad Edward 3 Färber, Michael 3 Fleuriot, Jacques D. 3 Höfner, Peter 3 Janičić, Predrag 3 Narboux, Julien 3 Niemetz, Aina 3 Parent, Xavier 3 Preiner, Mathias 3 Scott, Dana Stewart 3 Traytel, Dmitry 3 Viswanathan, Arjun 3 Waldmann, Uwe 3 Weber, Tjark 3 Wenzel, Makarius 3 Woltzenlogel Paleo, Bruno 3 Zeyda, Frank 2 Alama, Jesse 2 Armstrong, Alasdair 2 Berger, Ulrich 2 Bhayat, Ahmed 2 Bourke, Timothy 2 Bromberger, Martin 2 Bundy, Alan 2 Cavalcanti, Ana 2 Dubut, Jérémy 2 Fuenmayor, David 2 Grov, Gudmund 2 Johansson, Moa 2 Klein, Gerwin 2 Korovin, Konstantin 2 Lachnitt, Hanna 2 Lawrence, Andrew 2 Leino, K. Rustan M. 2 Lewis, Robert Y. 2 Nagashima, Yutaka 2 Nummelin, Visa 2 Pease, Alison 2 Raggi, Daniel 2 Roux, Cody 2 Schlichtkrull, Anders 2 Schulz, Stephan 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 Voronkov, Andrei 2 Yamada, Akihisa 1 Åman Pohjola, Johannes 1 Andreotti, Bruno 1 Back, Ralph-Johan 1 Banković, Milan 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 Bulwahn, Lukas 1 Buzzard, Kevin 1 Caminati, Marco Bright 1 Canham, Samuel 1 Cheney, James 1 Chiriţă, Claudia Elena 1 Claessen, Koen 1 Cristiá, Maximiliano ...and 122 more Authors all top 5 Cited in 21 Serials 37 Journal of Automated Reasoning 7 Journal of Logical and Algebraic Methods in Programming 5 Logical Methods in Computer Science 4 AI Communications 3 Formal Aspects of Computing 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 and Computation 1 Journal of Logic, Language and Information 1 Advances in Applied Clifford Algebras 1 Fundamenta Informaticae 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 20 Fields 167 Computer science (68-XX) 55 Mathematical logic and foundations (03-XX) 7 Combinatorics (05-XX) 3 Order, lattices, ordered algebraic structures (06-XX) 3 Category theory; homological algebra (18-XX) 2 General and overarching topics; collections (00-XX) 2 General algebraic systems (08-XX) 2 Geometry (51-XX) 1 History and biography (01-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 Probability theory and stochastic processes (60-XX) 1 Mechanics of particles and systems (70-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