A Learning-Based Fact Selector for Isabelle/HOL - Archive ouverte HAL Access content directly
Journal Articles Journal of Automated Reasoning Year : 2016

A Learning-Based Fact Selector for Isabelle/HOL

(1, 2, 3) , (4, 5) , (6) , (7) , (8)
1
2
3
4
5
6
7
8

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.
Fichier principal
Vignette du fichier
paper.pdf (286.52 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01386986 , version 1 (24-10-2016)

Identifiers

Cite

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

Altmetric

Share

Gmail Facebook Twitter LinkedIn More