Linking Isabelle with Automated Theorem Provers

This research programme culminated in the sledgehammer tool, which has become an indispensable part of Isabelle. With a single click, the Isabelle user can invoke several theorem provers, which will execute in the background and attempt to solve the current problem using all the information currently available in Isabelle. No other proof assistant has a similar tool. sledgehammer logo

View the poster!

  1. Jia Meng and L. C. Paulson.
    Experiments On Supporting Interactive Proof Using Resolution. In: David Basin and Michaël Rusinowitch (editors), IJCAR 2004: Second International Joint Conference on Automated Reasoning (Springer LNCS 3097, 2004), 372–384.
  2. Jia Meng, Claire Quigley and L. C. Paulson.
    Automation for Interactive Proof: First Prototype. Information and Computation 204 10 (2006), 1575–1596.
  3. Jia Meng and L. C. Paulson.
    Lightweight Relevance Filtering for Machine-Generated Resolution Problems. In: Geoff Sutcliffe, Renate Schmidt and Stephan Schulz (editors), ESCoR: Empirically Successful Computerized Reasoning (CEUR Workshop Proceedings, Vol. 192, 2006), 53–69. (See journal version below.)
  4. Jia Meng and L. C. Paulson.
    Translating Higher-Order Problems to First-Order Clauses. In: Geoff Sutcliffe, Renate Schmidt and Stephan Schulz (editors), ESCoR: Empirically Successful Computerized Reasoning (CEUR Workshop Proceedings, Vol. 192, 2006), 70–80.
  5. Jia Meng and L. C. Paulson.
    Lightweight Relevance Filtering for Machine-Generated Resolution Problems. J. Applied Logic 7 1 (2009), 41–57. Publisher's version
  6. L. C. Paulson and Kong Woei Susanto.
    Source-level proof reconstruction for interactive theorem proving.In: Klaus Schneider and Jens Brandt (editors), Theorem Proving in Higher Order Logics (Springer LNCS 4732, 2007), 232–245. Publisher's version. Slides available
  7. Jia Meng and L. C. Paulson.
    Translating Higher-Order Clauses to First-Order Clauses. J. Automated Reasoning 40 1 (2008), 35–60. Test data available. Publisher's version
  8. Jasmin Christian Blanchette, Sascha Böhme and L. C. Paulson.
    Extending Sledgehammer with SMT Solvers.
    In: Nikolaj Bjørner and Viorica Sofronie-Stokkermans (editors), 23rd International Conf. on Automated Deduction: CADE-23 (Springer LNAI 6803, 2011), 116–130. Publisher's version

You can also download experimental data:

This project was funded by the EPSRC [grant number GR/S57198/01].

Last revised: 28 August, 2014


Lawrence C. PaulsonComputer LaboratoryUniversity of Cambridge