8 October 2019 - Moa Johansson Abstract In this talk I will give a brief introduction to an automated lemma discovery technique called "Theory Exploration" as well as discussing some potential new directions, combining automated reasoning and machine learning. Theorem provers typically work by reasoning from a given set of facts, searching for a proof of a given conjecture. But what about situations where there are missing lemmas? This can be the case if we're trying to automating proofs by induction, as we don't necessarily have cut elimination. Theory exploration is a technique for inventing new and interesting mathematical conjectures, given a set of functions, constants and datatypes. I will show a demo of a system called Hipster, which not only automatically generates new conjectures (using testing), but also tries to prove them automatically, and finally assesses if the proof was interesting enough to motivate showing it to the human user. Finally, I will discuss potential improvements to automated reasoning, combining reasoning, theory exploration and machine learning. Oct 08 2019 15.00 - 16.00 8 October 2019 - Moa Johansson Theory Exploration - Reasoning, creativity and learning? 5.02, Bayes Centre
8 October 2019 - Moa Johansson Abstract In this talk I will give a brief introduction to an automated lemma discovery technique called "Theory Exploration" as well as discussing some potential new directions, combining automated reasoning and machine learning. Theorem provers typically work by reasoning from a given set of facts, searching for a proof of a given conjecture. But what about situations where there are missing lemmas? This can be the case if we're trying to automating proofs by induction, as we don't necessarily have cut elimination. Theory exploration is a technique for inventing new and interesting mathematical conjectures, given a set of functions, constants and datatypes. I will show a demo of a system called Hipster, which not only automatically generates new conjectures (using testing), but also tries to prove them automatically, and finally assesses if the proof was interesting enough to motivate showing it to the human user. Finally, I will discuss potential improvements to automated reasoning, combining reasoning, theory exploration and machine learning. Oct 08 2019 15.00 - 16.00 8 October 2019 - Moa Johansson Theory Exploration - Reasoning, creativity and learning? 5.02, Bayes Centre
Oct 08 2019 15.00 - 16.00 8 October 2019 - Moa Johansson Theory Exploration - Reasoning, creativity and learning?
