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 128 articles , 2 standard articles )

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

1 2 3 ... 5 6 7 next

  1. Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe: Superposition for lambda-free higher-order logic (2021)
  2. Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2021)
  3. 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)
  4. Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare: Towards satisfiability modulo parametric bit-vectors (2021)
  5. Popescu, Andrei; Traytel, Dmitriy: Distilling the requirements of Gödel’s incompleteness theorems with a proof assistant (2021)
  6. Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
  7. Benzmüller, Christoph; Fuenmayor, David: Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel’s ontological argument (2020)
  8. Benzmüller, Christoph; Parent, Xavier; van der Torre, Leendert: Designing normative theories for ethical and legal reasoning: \textscLogiKEyframework, methodology, and tool support (2020)
  9. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  10. Berghammer, Rudolf; Furusawa, Hitoshi; Guttmann, Walter; Höfner, Peter: Relational characterisations of paths (2020)
  11. Foster, Simon; Cavalcanti, Ana; Canham, Samuel; Woodcock, Jim; Zeyda, Frank: Unifying theories of reactive design contracts (2020)
  12. Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark: Extending SMT solvers to higher-order logic (2019)
  13. Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich: A formal proof of the expressiveness of deep learning (2019)
  14. Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2019)
  15. Färber, Michael; Kaliszyk, Cezary: Certification of nonclausal connection tableaux proofs (2019)
  16. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  17. Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare: Towards bit-width-independent proofs in SMT solvers (2019)
  18. Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
  19. Stojanović-Ðurđević, Sana: From informal to formal proofs in Euclidean geometry (2019)
  20. Wenzel, Makarius: Interaction with formal mathematical documents in Isabelle/PIDE (2019)

1 2 3 ... 5 6 7 next