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

Learning-Assisted Automated Reasoning

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

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

Abstract: 

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.