A Learning-Based Fact Selector for Isabelle/HOL
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef UrbanJournal of Automated Reasoning Volume 53, Number 3, pp. 219 – 244, 2016.
Abstract
Sledgehammer integrates automatic theorem provers in the proof assistant Isabelle/HOL. A key component, the fact selector, heuristically ranks the thousands of facts (lemmas, definitions, or axioms) available and selects a subset, based on syntactic similarity to the current proof goal. We introduce MaSh, an alternative that learns from successful proofs. New challenges arose from our ``zero click’‘ vision: MaSh integrates seamlessly with the users’ workflow, so that they benefit from machine learning without having to install software, set up servers, or guide the learning. MaSh outperforms the old fact selector on large formalizations.
BibTeX
@article{DBLP:journals/jar/BlanchetteGKKU16,
author = {Jasmin Christian Blanchette and
David Greenaway and
Cezary Kaliszyk and
Daniel K{\"{u}}hlwein and
Josef Urban},
title = {A Learning-Based Fact Selector for Isabelle/HOL},
journal = {J. Autom. Reasoning},
volume = {57},
number = {3},
pages = {219--244},
year = {2016},
url = {http://dx.doi.org/10.1007/s10817-016-9362-8},
doi = {10.1007/s10817-016-9362-8},
timestamp = {Mon, 05 Sep 2016 19:00:15 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/jar/BlanchetteGKKU16},
bibsource = {dblp computer science bibliography, http://dblp.org}
}