Automated Reasoning and AI for Large Formal Mathematics

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

• Josef Urban
• Friday 03 June 2016, 14:00-15:00
• William Gates Building - FW26.

If you have a question about this talk, please contact Louise Segar.

The first half of this talk will summarize several AI methods for learning and reasoning developed over large formal math corpora. We will show examples of AI systems implementing positive feedback loops between learning and deduction, and show the performance of the current methods over the Flyspeck, Isabelle, and Mizar libraries. The second half will discuss AI methods that we have recently started to develop for automating the translation of informal mathematics to formal. These methods combine statistical parsing of informal mathematics with the large-theory theorem proving methods.

This talk is part of the Machine Learning @ CUED series.

This talk is included in these lists:

• Seminar
• All Talks (aka the CURE list)
• Biology
• CBL important
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge Forum of Science and Humanities
• Cambridge Language Sciences
• Cambridge Neuroscience Seminars
• Cambridge talks
• Chris Davis' list
• Creating transparent intact animal organs for high-resolution 3D deep-tissue imaging
• Featured lists
• Guy Emerson's list
• Hanchen DaDaDash
• Inference Group Summary
• Information Engineering Division seminar list
• Interested Talks
• Joint Machine Learning Seminars
• Life Science
• Life Sciences
• ML
• Machine Learning @ CUED
• Machine Learning Summary
• Neuroscience
• Neuroscience Seminars
• Neuroscience Seminars
• Required lists for MLG
• Simon Baker's List
• Stem Cells & Regenerative Medicine
• Trust & Technology Initiative - interesting events
• William Gates Building - FW26
• bld31
• dh539
• kt532's list
• ndk22's list
• ob366-ai4er
• rp587
• yk373's list

Note that ex-directory lists are not shown.