Premise Selection and External Provers for HOL4

Thibault Gauthier and Cezary Kaliszyk

Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP 2015), pp. 49 – 57, 2015..


Learning-assisted automated reasoning has recently gained popularity among the users of Isabelle/HOL, HOL Light, and Mizar. In this paper, we present an add-on to the HOL4 proof assistant and an adaptation of the HOLyHammer system that provides machine learning-based premise selection and automated reasoning also for HOL4. We efficiently record the HOL4 dependencies and extract features from the theorem statements, which form a basis for premise selection. HOLyHammer transforms the HOL4 statements in the various TPTP-ATP proof formats, which are then processed by the ATPs.

We discuss the different evaluation settings: ATPs, accessible lemmas, and premise numbers. We measure the performance of HOLyHammer on the HOL4 standard library. The results are combined accordingly and compared with the HOL Light experiments, showing a comparably high quality of predictions. The system directly benefits HOL4 users by automatically finding proofs dependencies that can be reconstructed by Metis.


  PDF |    doi:10.1145/2676724.2693173  |  © ACM Open Access


author = "Thibault Gauthier and Cezary Kaliszyk",
title = "Premise Selection and External Provers for {HOL4}",
booktitle = "Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs",
editor = "Xavier Leroy and Alwen Tiu",
pages = "49--57",
year = 2015,
doi = "10.1145/2676724.2693173"
Nach oben scrollen