Exam questions from "Proof complexity and the P vs. NP problem".




You will get one question chosen at random from the following two:

  • (1) The feasible interpolation theorem for resolution and an exponential lower bound for R-refutations of the Clique-Color clauses.
    The non-automatizability of proof systems not admitting FI.

    [There are three different proofs in my 2019 book of the FI for R: Secs. 5.6, 17.6 (using 17.5) and 17.7; in lectures we covered the second. The lower bound argument is in Sec.13.5, the non-automatizability in Sec.17.3.]

  • (2) Ajtai's theorem: an exponential lower bound for constant depth Frege proofs of PHP.

    [This is in Sections 15.1-3 in the book.]