Wednesday Oct 5, 2022
Theoretical barriers for efficient proof search
(Susanna F. de Rezende, Lund University)
The proof search problem is a central question in automated theorem proving and SAT solving. Clearly, if a propositional tautology F does not have a short (polynomial size) proof in a proof system P, any algorithm that searches for P-proofs of F will necessarily take super-polynomial time. But can proofs of "easy" formulas, i.e., those that have polynomial size proofs, be found in polynomial time? This question motivates the study of automatability of proof systems. In this talk, we give an overview of known non-automatability results, focusing on the more recent ones, and present some of the main ideas used to obtain them.
For more information about the MIAO seminars, please see http://www.jakobnordstrom.se/videoseminars/ .
Theoretical barriers for efficient proof search
(Susanna F. de Rezende, Lund University)
The proof search problem is a central question in automated theorem proving and SAT solving. Clearly, if a propositional tautology F does not have a short (polynomial size) proof in a proof system P, any algorithm that searches for P-proofs of F will necessarily take super-polynomial time. But can proofs of "easy" formulas, i.e., those that have polynomial size proofs, be found in polynomial time? This question motivates the study of automatability of proof systems. In this talk, we give an overview of known non-automatability results, focusing on the more recent ones, and present some of the main ideas used to obtain them.
For more information about the MIAO seminars, please see http://www.jakobnordstrom.se/videoseminars/ .
Comments