×

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
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

Citations by Year