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 Lawrence C Paulson
[go: Go Back, main page]

Linking Isabelle with Automated Theorem Provers

  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. Journal of Applied Logic, in press.
  6. L. C. Paulson and Kong Woei Susanto.
    Source-level proof reconstruction for interactive theorem proving. In: Jens Brandt (editor), Theorem Proving in Higher Order Logics (2007), in press.

You can also download experimental data:

Research funded by the EPSRC grant GR/S57198/01, Automation for Interactive Proof.