HOL4的前提选择与外部证明器
人工智能
2015-09-14 v1
摘要
学习辅助的自动化推理近期在Isabelle/HOL、HOL Light和Mizar的用户中获得了流行。在本文中，我们提出一个HOL4证明助手的附加组件以及对HOLyHammer系统的改造，其为HOL4也提供基于机器学习的前提选择与自动化推理。我们高效记录HOL4依赖关系并从定理陈述中提取特征，这些构成了前提选择的基础。HOLyHammer将HOL4陈述转换为多种TPTP-ATP证明格式，随后由ATPs处理。我们讨论了不同的评估设置：ATPs、可访问引理与前提数量。我们度量了HOLyHammer在HOL4标准库上的性能。结果被相应合并并与HOL Light实验比较，显示出可比较的高预测质量。该系统通过自动发现可由Metis重建的证明依赖关系，直接惠及HOL4用户。
引用
@article{arxiv.1509.03534,
title = {Premise Selection and External Provers for HOL4},
author = {Thibault Gauthier and Cezary Kaliszyk},
journal= {arXiv preprint arXiv:1509.03534},
year = {2015}
}