Talks and Poster Presentations (with Proceedings-Entry):
J. Jakubuv, M. Suda, J. Urban:
"Automated Invention of Strategies and Term Orderings for Vampire";
Talk: GCAI 2017 / 3rd Global Conference on Artificial Intelligence,
Miami, USA;
2017-10-19
- 2017-10-22; in: "GCAI 2017. 3rd Global Conference on Artificial Intelligence",
EasyChair EPiC Series in Computing,
Volume 50
(2017),
121
- 133.
English abstract:
In this work we significantly increase the performance of the Vampire and E automated theorem provers (ATPs) on a set of loop theory problems. This is done by developing EmpireTune, an AI system that automatically invents targeted search strategies for Vampire and E. EmpireTune extends previous strategy invention systems in several ways. We have developed support for the Vampire prover, further extended Vampire by new mechanisms for specifying term orderings, and EmpireTune can now automatically invent suitable term ordering for classes of problems. We describe the motivation behind these additions, their implementation in Vampire and EmpireTune, and evaluate the systems with very good results on the AIM (loop theory) ATP benchmark.
Keywords:
automated theorem proving, proving strategy, strategy invention, first-order logic, machine learning, parameters learning
Electronic version of the publication:
http://publik.tuwien.ac.at/files/publik_264656.pdf
Created from the Publication Database of the Vienna University of Technology.