Event details

Speaker: Dr Michael Rawson, New Frontiers Fellow. I became interested in automated reasoning when using a proof assistant for my bachelor’s thesis. The proof automation failed sometimes on easy problems, seemingly at random. How hard could it be? Since then I’ve finished a PhD in machine learning for automated reasoning and a postdoc in parallel theorem proving at Manchester, then another postdoctoral stint in Vienna improving the state of the art in theorem proving and working on various applications of the technology. Recently I am very pleased to join the Cyber Physical Systems group here at Southampton.

Abstract: Automated reasoning is one of the oldest endeavours in computer science, but it is not as widely known or used as it might be. Perhaps it could help you with something! I will lay out the “big picture” of automated reasoning systems: what they can do, what they can’t, where they excel and where they struggle, and some case-study applications. Then I’ll go into some depth about the challenges and solutions involved in my own corner, automated theorem proving for first-order logic, and demonstrate Vampire, a world-class fully-automatic theorem prover.