Output details
11 - Computer Science and Informatics
University of Cambridge
Article title
Translating higher-order clauses to first-order clauses
Type
D - Journal article
Title of journal
J AUTOM REASONING
Article number
-
Volume number
40
Issue number
1
First page of article
35
ISSN of journal
0168-7433
Year of publication
2008
URL
-
Number of additional authors
1
Additional information
<11> Isabelle's Sledgehammer tool, which invokes external theorem provers to solve goals arising during interactive proof, is now heavily used. This paper reports one of the crucial empirical studies that made Sledgehammer effective with higher-order logic formulas. At the conference IJCAR 2012, Isabelle (equipped with an updated version of these techniques) won the higher-order division of the automated systems competition (CASC). See http://www.cs.miami.edu/~tptp/CASC/J6/WWWFiles/DivisionSummary1.html
It also led to follow-on research at the Technical University of Munich and at Cambridge.
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Citation count
32
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
