Skip to Main content Skip to Navigation
Journal articles

A Learning-Based Fact Selector for Isabelle/HOL

Abstract : Sledgehammer integrates automatic theorem provers in the proof assistant Isa-belle/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.
Document type :
Journal articles
Complete list of metadata

Cited literature [53 references]  Display  Hide  Download
Contributor : Jasmin Blanchette Connect in order to contact the contributor
Submitted on : Monday, October 24, 2016 - 11:43:23 PM
Last modification on : Wednesday, November 3, 2021 - 7:09:20 AM


Files produced by the author(s)




Jasmin Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban. A Learning-Based Fact Selector for Isabelle/HOL. Journal of Automated Reasoning, Springer Verlag, 2016, 57, pp.219 - 244. ⟨10.1007/s10817-016-9362-8⟩. ⟨hal-01386986⟩



Les métriques sont temporairement indisponibles