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.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2016, 57, pp.219 - 244. 〈10.1007/s10817-016-9362-8〉
Liste complète des métadonnées

Littérature citée [53 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01386986
Contributeur : Jasmin Christian Blanchette <>
Soumis le : lundi 24 octobre 2016 - 23:43:23
Dernière modification le : mercredi 26 octobre 2016 - 01:11:35

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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〉

Partager

Métriques

Consultations de
la notice

105

Téléchargements du document

87