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.


References in zbMATH (referenced in 139 articles , 2 standard articles )

Showing results 1 to 20 of 139.
Sorted by year (citations)

1 2 3 ... 5 6 7 next

  1. Bonacina, Maria Paola; Graham-Lengrand, Stéphane; Shankar, Natarajan: Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (2022)
  2. Dalvandi, Sadegh; Dongol, Brijesh; Doherty, Simon; Wehrheim, Heike: Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL (2022)
  3. Dubut, Jérémy; Yamada, Akihisa: Fixed points theorems for non-transitive relations (2022)
  4. Wieser, Eric; Song, Utensil: Formalizing geometric algebra in Lean (2022)
  5. Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe: Superposition for lambda-free higher-order logic (2021)
  6. Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2021)
  7. Bromberger, Martin; Dragoste, Irina; Faqeh, Rasha; Fetzer, Christof; Krötzsch, Markus; Weidenbach, Christoph: A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (2021)
  8. Foster, Simon; Nemouchi, Yakoub; Gleirscher, Mario; Wei, Ran; Kelly, Tim: Integration of formal proof into unified assurance cases with Isabelle/SACM (2021)
  9. From, Asta Halkjær; Eschen, Agnes Moesgård; Villadsen, Jørgen: Formalizing axiomatic systems for propositional logic in Isabelle/HOL (2021)
  10. Guan, Yong; Zhang, Jingzhi; Wang, Guohui; Li, Ximeng; Shi, Zhiping; Li, Yongdong: Formalization of Euler-Lagrange equation set based on variational calculus in HOL light (2021)
  11. Holden, Edvard K.; Korovin, Konstantin: Heterogeneous heuristic optimisation and scheduling for first-order theorem proving (2021)
  12. Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare: Towards satisfiability modulo parametric bit-vectors (2021)
  13. Popescu, Andrei; Traytel, Dmitriy: Distilling the requirements of Gödel’s incompleteness theorems with a proof assistant (2021)
  14. Rawson, Michael; Reger, Giles: \textsflazyCoP: lazy paramodulation meets neurally guided search (2021)
  15. Schurr, Hans-Jörg; Fleury, Mathias; Desharnais, Martin: Reliable reconstruction of fine-grained proofs in a proof assistant (2021)
  16. Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
  17. Sutcliffe, Geoff; Desharnais, Martin: The CADE-28 automated theorem proving system competition -- CASC-28 (2021)
  18. Benzmüller, Christoph; Fuenmayor, David: Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel’s ontological argument (2020)
  19. Benzmüller, Christoph; Parent, Xavier; van der Torre, Leendert: Designing normative theories for ethical and legal reasoning: \textscLogiKEyframework, methodology, and tool support (2020)
  20. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)

1 2 3 ... 5 6 7 next