مقاله Premise Selection for Mathematics by Corpus Analysis and Kernel Methods : تی پی بین

خلاصه مقاله

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.

نویسندگان

Jesse Alama [ Center for Artificial Intelligence, New University of Lisbon, 1099085, Lisbon, Portugal ]

Tom Heskes [ Intelligent Systems, Institute for Computing and Information Sciences, Radboud University, Nijmegen, Netherlands ]

Daniel Kühlwein [ Intelligent Systems, Institute for Computing and Information Sciences, Radboud University, Nijmegen, Netherlands ]

Evgeni Tsivtsivadze [ Intelligent Systems, Institute for Computing and Information Sciences, Radboud University, Nijmegen, Netherlands ]

Josef Urban [ Intelligent Systems, Institute for Computing and Information Sciences, Radboud University, Nijmegen, Netherlands ]

کلمات کلیدی

Automated reasoning in large theories Machine learning Premise selection Automated theorem proving

آدرس این مقاله

آدرس مستقیم دسترسی به این مقاله

مشخصات کنفرانس

مشاهده مقالات

Journal of Automated Reasoning 2013

The interdisciplinary Journal of Automated Reasoning balances theory, implementation and application. The spectrum of coverage ranges from the presentation of a new inference rule with proof of its logical properties to a detailed account of a computer program designed to solve various problems in industry. Topics include automated theorem proving, logic programming, expert systems, program synthesis and validation, artificial intelligence, computational logic, robotics, and various industrial applications. The contents focus on several aspects of automated reasoning, a field whose objective is the design and implementation of a computer program that serves as an assistant in solving problems and in answering questions that require reasoning. The Journal of Automated Reasoning provides a forum and a means for exchanging information for those interested purely in theory, those interested primarily in implementation, and those interested in specific research and industrial applications.

حوزه های تحت پوشش : automated theorem proving, logic programming, expert systems, program synthesis and validation, artificial intelligence, computational logic, robotics, and various industrial applications