For any unsatisfiable CNF formula we give an exponential lower bound on the size of resolution refutations of a propositional statement that the formula has a resolution refutation. We describe three applications. (1) An open question in [Atserias-Müller,2019] asks whether a certain natural propositional encoding of the above statement is ... more >>>

We show that for every integer $k \geq 2$, the Res($k$) propositional proof system does not have the weak feasible disjunction property. Next, we generalize a recent result of Atserias and Müller [FOCS, 2019] to Res($k$). We show that if NP is not included in P (resp. QP, SUBEXP) then ... more >>>

We propose a diagonalization-based approach to several important questions in proof complexity. We illustrate this approach in the context of the algebraic proof system IPS and in the context of propositional proof systems more generally.

We give an explicit sequence of CNF formulas $\{\phi_n\}$ such that VNP$\neq$VP iff there are ... more >>>

Connections between proof complexity and circuit complexity have become major tools for obtaining lower bounds in both areas. These connections -- which take the form of interpolation theorems and query-to-communication lifting theorems -- translate efficient proofs into small circuits, and vice versa, allowing tools from one area to be applied ... more >>>