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

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

1 2 3 4 5 6 next

  1. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  2. Avigad, Jeremy (ed.); Blanchette, Jasmin Christian (ed.); Klein, Gerwin (ed.); Paulson, Lawrence (ed.); Popescu, Andrei (ed.); Snelting, Gregor (ed.): Introduction to “Milestones in interactive theorem proving” (2018)
  3. Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2018)
  4. Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2018)
  5. Blanchette, Jasmin Christian; Peltier, Nicolas; Robillard, Simon: Superposition with datatypes and codatatypes (2018)
  6. Boulmé, Sylvain; Maréchal, Alexandre: A Coq tactic for equality learning in linear arithmetic (2018)
  7. Guttmann, Walter: An algebraic framework for minimum spanning tree problems (2018)
  8. Guttmann, Walter: Verifying minimum spanning tree algorithms with Stone relation algebras (2018)
  9. Lopez Hernandez, Julio Cesar; Korovin, Konstantin: An abstraction-refinement framework for reasoning with large theories (2018)
  10. Paulson, Lawrence C.: Computational logic: its origins and applications (2018)
  11. Reynolds, Andrew; Viswanathan, Arjun; Barbosa, Haniel; Tinelli, Cesare; Barrett, Clark: Datatypes with shared selectors (2018)
  12. Sato, Yuri; Wajima, Yuichiro; Ueda, Kazuhiro: Strategy analysis of non-consequence inference with Euler diagrams (2018)
  13. Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2018)
  14. Avigad, Jeremy; Hölzl, Johannes; Serafin, Luke: A formally verified proof of the central limit theorem (2017)
  15. Beeson, Michael; Wos, Larry: Finding proofs in Tarskian geometry (2017)
  16. Berghammer, Rudolf; Guttmann, Walter: An algebraic approach to multirelations and their properties (2017)
  17. Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Soundness and completeness proofs by coinductive methods (2017)
  18. Cheney, James; Momigliano, Alberto: (\alpha\mathrmCheck): a mechanized metatheory model checker (2017)
  19. Foster, Simon; Thiele, Bernhard; Cavalcanti, Ana; Woodcock, Jim: Towards a UTP semantics for Modelica (2017)
  20. Guttmann, Walter: Stone relation algebras (2017)

1 2 3 4 5 6 next