ACL2 Seminar, March 8, 2019

Speaker: Marijn Heule
Title: Solving Hard Problems Automatically

Abstract:

No matter what scientific field we look at today, there is no lack of
hard problems whose solutions seem completely out of reach. In
mathematics alone, we can easily find countless questions that have
been open for decades; but also in computer science and biology,
researchers have been looking at problems that, so far, have brought
even the greatest minds to their knees. Many of these problems are not
only of theoretical interest, their solutions would also have
significant practical implications.

Luckily, we are now at a point where automated reasoning has become
mature enough to help us solve these problems. In my talk, I show how
automated reasoning techniques have been crucial in tackling hard open
problems from various fields, including mathematics, bioinformatics,
and software engineering. I focus on several of my contributions,
including mechanizing abstract reasoning and effectively parallelizing
the big computations. I also address the issue of why we can have
confidence in the correctness of the answers produced by today's
automated reasoning tools. To complete the picture, I discuss popular
open problems whose solutions could potentially be obtained by
capitalizing on the power of automated reasoning.