期刊
JOURNAL OF AUTOMATED REASONING
卷 52, 期 2, 页码 191-213出版社
SPRINGER
DOI: 10.1007/s10817-013-9286-5
关键词
Automated reasoning in large theories; Machine learning; Premise selection; Automated theorem proving
资金
- FCT project Dialogical Foundations of Semantics (DiFoS) in the ESF EuroCoRes programme LogICCC [FCT LogICCC/0001/2007]
- NWO
Smart premise selection is essential when using automated reasoning as a tool for large-theory formal proof development. This work develops learning-based premise selection in two ways. First, a fine-grained dependency analysis of existing high-level formal mathematical proofs is used to build a large knowledge base of proof dependencies, providing precise data for ATP-based re-verification and for training premise selection algorithms. Second, a new machine learning algorithm for premise selection based on kernel methods is proposed and implemented. To evaluate the impact of both techniques, a benchmark consisting of 2078 large-theory mathematical problems is constructed, extending the older MPTP Challenge benchmark. The combined effect of the techniques results in a 50 % improvement on the benchmark over the state-of-the-art Vampire/SInE system for automated reasoning in large theories.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据