TY - JOUR
T1 - A Learning-Based Fact Selector for Isabelle/HOL
AU - Blanchette, J.C.
AU - Greenaway, David
AU - Kaliszyk, Cezary
AU - Kühlwein, Daniel
AU - Urban, Josef
PY - 2016/10/1
Y1 - 2016/10/1
N2 - 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.
AB - 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.
KW - Automatic theorem provers
KW - Machine learning
KW - Proof assistants
KW - Relevance filtering
UR - http://www.scopus.com/inward/record.url?scp=84957604800&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/record.url?scp=84957604800&partnerID=8YFLogxK
U2 - 10.1007/s10817-016-9362-8
DO - 10.1007/s10817-016-9362-8
M3 - Article
SN - 0168-7433
VL - 57
SP - 219
EP - 244
JO - Journal of Automated Reasoning
JF - Journal of Automated Reasoning
IS - 3
ER -