通过学习子句引导锤击 Mizar
人工智能
2019-04-04 v1 机器学习
计算机科学中的逻辑
摘要
我们描述了一种通过结合学习与定理证明，对现有基于大型ITP库的锤击式证明自动化进行的极大改进。具体而言，我们将最先进的机器学习器集成到E自动定理证明器中，并开发了能够在整个Mizar库上实现E的学习与高效内部引导的方法。所得到的训练系统在单一策略设置下将E在Mizar库上的实时性能提升了70%。
引用
@article{arxiv.1904.01677,
title = {Hammering Mizar by Learning Clause Guidance},
author = {Jan Jakubův and Josef Urban},
journal= {arXiv preprint arXiv:1904.01677},
year = {2019}
}
备注
arXiv admin note: substantial text overlap with arXiv:1903.03182