Machine Learning for Interactive Theorem Proving: Revisit, Reuse and Recycle your Proofs

Add to your list(s) Download to your calendar using vCal

• Katya Komendenskaya (Heriot-Watt University)
• Thursday 13 July 2017, 16:00-17:00
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact INI IT.

BPRW01 - Computer-aided mathematical proof

Interactive theorem proving has seen major development in the past decade,  and is being  widely adopted in formalisation of mathematics and in verification. Further growth and dissemination of interactive theorem proving  require more intelligent tools that can make this technology more user friendly and convenient. As full automation of interactive provers is impossible, it is important to develop better heuristics that enableto data mine the existing libraries and  reuse existing proof strategies when writing new proofs.In this talk, I will talk about several projects devoted to Machine Learning for Interactive Theorem Proving (in Coq and ACL2 )  that I participated in in the last 5 years.I will give a light survey of a variety of machine learning methods that have already been employed in these provers, and will discuss, with some help from the audience, which of those methods bear more promise for the future. In the technical part, I will also talk about ML4PG —  the machine learning extension to Proof general, that I have developed in collaboration with  my colleagues, its recent extension Coq-PR3 and the plans to re-incarnate these tools in the upcoming new version of Proof General currently developed by INRIA and at MIT .    Based on the joint work with G.Grov,  T.Gransden,  J.Heras, M.Johansson, E.McLean, N.Walkinshaw.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.