Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Publications of L C Paulson: Sledgehammer
[go: Go Back, main page]

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.

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

You can also download experimental data:

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