Thursday, 8th of March 2018, 12:00 – 1:00

Learning-Assisted Automated Reasoning

SR 1, ICT Building,
Technikerstraße 21a, 6020 Innsbruck

Michael Färber
Researcher at CL group, University of Innsbruck


Interactive proof assistants (ITPs) are programs that aid users writing machine-verified proofs. To improve user experience, there are so-called "hammer" systems for ITPs that aim to find proofs automatically. I show ongoing work to improve hammer systems, including machine learning techniques such as random forests and Monte Carlo Tree Search, as well as the integration of new automatic proof search methods.