Show menu

Susanna F. de Rezende: Theoretical barriers for efficient proof search

Thanks! Share it with your friends!

You disliked this video. Thanks for the feedback!


Added by
49 Views
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/ .

Post your comment

Comments

Be the first to comment

Up Next