Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4662922 | Journal of Applied Logic | 2013 | 12 Pages |
Abstract
Sledgehammer is a tool that harnesses external first-order automatic theorem provers (ATPs) to discharge interactive proof obligations arising in Isabelle/HOL. We extended it with LEO-II and Satallax, the two most prominent higher-order ATPs, improving its performance on higher-order problems. To explore their usefulness, these ATPs are measured against first-order ATPs and built-in Isabelle tactics on a variety of benchmarks from Isabelle and the TPTP library. Sledgehammer provides an ideal test bench for individual features of LEO-II and Satallax, revealing areas for improvements.
Keywords
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Nik Sultana, Jasmin Christian Blanchette, Lawrence C. Paulson,