cl-banner

Lemma Mining over HOL Light

Cezary Kaliszyk and Josef Urban

Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-19), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 8312, pp. 503 – 517, 2013.

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.

 

  PDF |    doi:10.1007/978-3-642-45221-5_34

BibTeX 

@inproceedings{CKJU-LPAR19,
author = "Cezary Kaliszyk and Josef Urban",
title = "Lemma Mining over {HOL} Light",
booktitle = "Proceedings of the 19th International Conference on Logic
for Programming, Artificial Intelligence, and Reasoning",
series = "Lecture Notes in Computer Science (Advanced Research in
Computing and Software Science)",
editor = "Kenneth L. McMillan and Aart Middeldorp and Andrei Voronkov",
volume = 8312,
pages = "503--517",
year = 2013,
doi = "10.1007/978-3-642-45221-5_34"
}
Nach oben scrollen