Published in

Elsevier, Journal of Applied Logic, 1(11), p. 91-102

DOI: 10.1016/j.jal.2012.12.002

Links

Tools

Export citation

Search in Google Scholar

LEO-II and Satallax on the Sledgehammer test bench

Journal article published in 2013 by Nik Sultana, Jasmin Christian Blanchette, Lawrence C. Paulson
This paper is made freely available by the publisher.
This paper is made freely available by the publisher.

Full text: Download

Green circle
Preprint: archiving allowed
Upload
Red circle
Postprint: archiving forbidden
Red circle
Published version: archiving forbidden
Policy details
Data provided by SHERPA/RoMEO

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.