Speaker: Susanna F. de Rezende (Czech Academy of Sciences)

Title: Automatability of Tree-like Proof Systems 

Abstract: Intuitively, automatability addresses the proof search problem: How hard is it to find a proof? Given an unsatisfiable formula F that has a polynomial size refutation, can we find a refutation of F in polynomial time? Formally, a proof system P is automatable if there is an algorithm that given an unsatisfiable formula F, outputs a P-refutation of F in time polynomial in the size of the smallest P-refutation of F plus the size of F. In this talk, we will discuss what is known about automatability of tree-like proof systems. In particular, we will consider tree-like resolution, for which the question of automatability is, under ETH, essentially settled; tree-like Res(k), for which a similar tight result can be obtained; and tree-like Res(parity) and tree-like cutting planes, for which we only have partial results.