Lemma Mining over HOL Light
From MaRDI portal
Abstract: Large formal mathematical libraries consist of millions of atomic inference steps that give rise to a corresponding number of proved statements (lemmas). Analogously to the informal mathematical practice, only a tiny fraction of such statements is named and re-used in later proofs by formal mathematicians. In this work, we suggest and implement criteria defining the estimated usefulness of the HOL Light lemmas for proving further theorems. We use these criteria to mine the large inference graph of all lemmas in the core HOL Light library, adding thousands of the best lemmas to the pool of named statements that can be re-used in later proofs. The usefulness of the new lemmas is then evaluated by comparing the performance of automated proving of the core HOL Light theorems with and without such added lemmas.
Recommendations
- scientific article; zbMATH DE number 7594146
- PRocH: proof reconstruction for HOL Light
- An Interpretation of Isabelle/HOL in HOL Light
- Light monotone Dialectica methods for proof mining
- New light on Hensel's Lemma
- Proving Valid Quantified Boolean Formulas in HOL Light
- Conversion of HOL Light proofs into Metamath
- A lantern lemma
- Steps towards Verified Implementations of HOL Light
- An Isabelle-like procedural mode for HOL Light
Cited in
(9)- JEFL: joint embedding of formal proof libraries
- Matching concepts across HOL libraries
- Proof mining with dependent types
- What's in a theorem name?
- scientific article; zbMATH DE number 7594146 (Why is no real title available?)
- Lemmatization for stronger reasoning in large theories
- HOL(y)Hammer: online ATP service for HOL Light
- Learning-assisted theorem proving with millions of lemmas
- Toward a procedure for data mining proofs
Describes a project that uses
Uses Software
This page was built for publication: Lemma Mining over HOL Light
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2870150)
