Sledgehammer
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.
Keywords for this software
References in zbMATH (referenced in 49 articles , 2 standard articles )
Showing results 1 to 20 of 49.
Sorted by year (- Beeson, Michael; Wos, Larry: Finding proofs in Tarskian geometry (2017)
- Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Soundness and completeness proofs by coinductive methods (2017)
- Reynolds, Andrew; Blanchette, Jasmin Christian: A decision procedure for (co)datatypes in SMT solvers (2017)
- Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
- Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
- Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)
- Blanchette, Jasmin Christian; Fleury, Mathias; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2016)
- Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
- Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Mechanizing a process algebra for network protocols (2016)
- Guttmann, Walter: An algebraic approach to computations with progress (2016)
- Raggi, Daniel; Bundy, Alan; Grov, Gudmund; Pease, Alison: Automating change of representation for proofs in discrete mathematics (extended version) (2016)
- Zhan, Bohua: AUTO2, A saturation-based heuristic prover for higher-order logic (2016)
- Berger, Ulrich; Lawrence, Andrew; Forsberg, Fredrik Nordvall; Seisenberger, Monika: Extracting verified decision procedures: DPLL and resolution (2015)
- Berghammer, Rudolf; Guttmann, Walter: Closure, properties and closure properties of multirelations (2015)
- Foster, Simon; Struth, Georg: On the fine-structure of regular algebra (2015)
- Guttmann, Walter: Infinite executions of lazy and strict computations (2015)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
- Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei: A first class Boolean sort in first-order theorem proving and TPTP (2015)
- Preoteasa, Viorel; Back, Ralph-Johan; Eriksson, Johannes: Verification and code generation for invariant diagrams in Isabelle (2015)
- Reger, Giles; Tishkovsky, Dmitry; Voronkov, Andrei: Cooperating proof attempts (2015)