Skip to main content
SpringerLink
Log in

Sledgehammer: Judgement Day

  • Conference paper
  • First Online:
Book cover Automated Reasoning (IJCAR 2010)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6173))

Included in the following conference series:

Abstract

Sledgehammer, a component of the interactive theorem prover Isabelle, finds proofs in higher-order logic by calling the automated provers for first-order logic E, SPASS and Vampire. This paper is the largest and most detailed empirical evaluation of such a link to date. Our test data consists of 1240 proof goals arising in 7 diverse Isabelle theories, thus representing typical Isabelle proof obligations. We measure the effectiveness of Sledgehammer and many other parameters such as run time and complexity of proofs. A facility for minimizing the number of facts needed to prove a goal is presented and analyzed.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bradley, A., Manna, Z.: Property-directed incremental invariant generation. Formal Asp. Comput. 20, 379–405 (2008)

    Article  Google Scholar 

  2. Huang, X.: Reconstructing proofs at the assertion level. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 738–752. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  3. Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Muñoz, C. (eds.) Design and Application of Strategies/Tactics in Higher Order Logics. Number NASA/CP-2003-212448 in NASA Technical Reports, pp. 56–68 (2003)

    Google Scholar 

  4. Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Automated Reasoning 40, 35–60 (2008)

    Article  MathSciNet  Google Scholar 

  5. Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic 7, 41–57 (2009)

    Article  MathSciNet  Google Scholar 

  6. Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002), http://www.in.tum.de/~nipkow/LNCS2283/

    Book  Google Scholar 

  7. Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 232–245. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  8. Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15, 91–110 (2002)

    MATH  Google Scholar 

  9. Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2-3), 111–126 (2002)

    MATH  Google Scholar 

  10. Sutcliffe, G.: SystemOnTPTP. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 406–410. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  11. Sutcliffe, G.: The 4th IJCAR Automated Theorem Proving System Competition — CASC-J4. AI Commun. 22, 59–72 (2009)

    Article  MathSciNet  Google Scholar 

  12. Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP Data-Exchange Formats for Automated Theorem Proving Tools. In: Sorge, V., Zhang, W. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, pp. 201–215. IOS Press, Amsterdam (2004)

    Google Scholar 

  13. Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Automated Reasoning 37(1-2), 21–43 (2006)

    Article  Google Scholar 

  14. Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: Spass version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009)

    Google Scholar 

  15. Wenzel, M.: Isar — a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Thery, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167–183. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  16. Wos, L., Robinson, G., Carson, D.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12, 536–541 (1965)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Technische Universität München, Germany

    Sascha Böhme & Tobias Nipkow

Authors
  1. Sascha Böhme
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tobias Nipkow
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. RWTH Aachen, LuFG Informatik, 2, Ahornstr. 55, 52074, Aachen, Germany

    Jürgen Giesl

  2. Department of Computer Science, Chalmers University of Technology, 41296, Gothenburg, Sweden

    Reiner Hähnle

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Böhme, S., Nipkow, T. (2010). Sledgehammer: Judgement Day. In: Giesl, J., Hähnle, R. (eds) Automated Reasoning. IJCAR 2010. Lecture Notes in Computer Science(), vol 6173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14203-1_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14203-1_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14202-4

  • Online ISBN: 978-3-642-14203-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation