BriefGPT.xyz
Sep, 2015
HOL4的前提选择和外部证明器
Premise Selection and External Provers for HOL4
HTML
PDF
Thibault Gauthier, Cezary Kaliszyk
TL;DR
本文提出HOL4证明助手的机器学习辅助自动推理和前提选择方法，从定理陈述中提取特征选取前提，通过HOLyHammer将其转换为不同格式，再经由ATPs处理。实验显示该系统在HOL4标准库上具有较高的性能。
Abstract
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
→