LEO-II and Satallax on the Sledgehammer test bench |
| |
Authors: | Nik Sultana Jasmin Christian Blanchette Lawrence C. Paulson |
| |
Affiliation: | 1. Computer Laboratory, University of Cambridge, United Kingdom;2. Institut für Informatik, Technische Universität München, Germany |
| |
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: | |
本文献已被 ScienceDirect 等数据库收录! |
|