Linking Isabelle with Automated Theorem Provers

This research programme culminated in the sledgehammer tool, which has become an indispensable part of Isabelle. That work was complete by 2007; subsequent substantial improvements were made by Jasmin Christian Blanchette and his colleagues.

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. Sledgehammer is extensively used, and has opened up new branches of research into linking different theorem provers and coping with very large axiom sets.

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. Publisher's version
  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. Publisher's version
  8. Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. PAAR-2010: Workshop on Practical Aspects of Automated Reasoning. Edinburgh, Scotland, July 2010. (Talk given by Jasmin Christian Blanchette.) An updated version appeared in G. Sutcliffe, E. Ternovska, and S. Schulz (eds) 8th International Workshop on the Implementation of Logics (IWIL-2010). Yogyakarta, Indonesia, October 2010.
  9. 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

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