Proof complexity and the P vs. NP problem
Jan Krajicek


Original bibliography page for the course

References for Part 1

Books and lecture notes:
My 1995 book and the lecture notes listed below contain essentially all material covered in Parts 1 and 2 (with the exceptions of some examples of proof systems - these are in my 2005 surveys listed below - and of the applications of reflection principles to SAT algorithms).

  • P.Clote and E.Kranakis, Boolean functions and computation models, Springer, 2002.

  • S.A.Cook, a set of lecture notes, 1973.

  • S.A.Cook and P.Nguyen, Logical Foundations of Proof Complexity, Cambridge U.Press, 2010.

  • J.Krajicek, Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press, 1995.

  • J.Krajicek, Forcing with random variables and proof complexity, CUP, 2011.
    [Chpt.27 overviews some of proof complexity]

  • J.Krajicek, Propositional proof complexity I. a Proof complexity and arithmetic, two sets of lecture notes.
    Papers:
  • Sam Buss, Towards NP-P via Proof Complexity and Search, preliminary manuscript. 2009.

  • S.A.Cook, The Complexity of Theorem Proving Procedures, Proc. of the 3rd Annual ACM Symposium on Theory of Computing, pp.151-158, (May 1971).

  • S.A.Cook and R.A.Reckhow, The Relative Efficiency of Propositional Proof Systems, J. Symbolic Logic, 44(1), pp.36-50, (1979). Their older paper.

  • J.Krajicek, "Proof complexity, in: Laptev, A. (ed.), European congress of mathematics (ECM), Stockholm, Sweden, June 27--July 2, 2004. Zurich: European Mathematical Society, (2005), pp.221-231. Pdf file.

  • J.Krajicek, "Hardness assumptions in the foundations of theoretical computer science", Archive for Mathematical Logic, 44(6)}, (2005), pp.667-675.
    Pdf file.

  • J.Krajicek, "From feasible proofs to feasible computations", in: Computer Science Logic 2010, A. Dawar and H. Veith (Eds.), LNCS 6247, Springer, Heidelberg (2010), pp.22-31.
    [contains overview of witnessing, propositional translation done a bit differently, feasible interpolation, etc.]

  • P. Pudlak: The lengths of proofs, in Handbook of Proof Theory, S.R. Buss ed., Elsevier, 1998, pp.547-637.

    References specific to Part 2:

  • S.A.Cook, Feasibly constructive proofs and the propositional calculus , Proc. of 7th annual ACM symposium on Theory of computing, Albuerque, New Mexico, pp.83-97, (1975).

  • S.A.Cook and J.Krajicek, Consequences of the provability of NP \subseteq P/poly, 72(4), (2007), pp. 1353-1371.

  • J.Krajicek and P.Pudlak: "Propositional Proof Systems, the Consistency of First Order Theories and the Complexity of Computations", J. Symbolic Logic, 54(3), (1989), pp. 1063-1079.
    [This introduces and discusses the problem of the existence of an optimal proof system, including the links to finitistic Godel's thm. References about the finitistic Godels' thm can be found among the references for my Spring 2011 course.]

    References for Part 3:

  • A.Atserias and M. L. Bonet, On the Automatizability of Resolution and Related Propositional Proof Systems, Information and Computation, 189(2), (2004), pp.182-201.

  • M.L.Bonet, T.Pitassi, and R.Raz (2000), On Interpolation and Automatization for Frege Proof Systems, SIAM Journal of Computing, 29 (6):1939-1967.

  • J.Krajicek, "Lower Bounds to the Size of Constant-Depth Propositional Proofs", J. of Symbolic Logic, 59(1), (1994), pp.73-86.

  • J.Krajicek, "On methods for proving lower bounds in propositional logic", in: {\em Logic and Scientific Methods} Eds. M. L. Dalla Chiara et al., (Vol. 1 of Proc. of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence (August 19-25, 1995)), Synthese Library, Vol.259, Kluwer Academic Publ., Dordrecht, (1997), pp.69-83.

  • J.Krajicek, "Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic", J. of Symbolic Logic, {\bf 62(2)}, (1997), pp.457-486.

  • J.Krajicek, Diagonalization in proof complexity, Fundamenta Mathematicae, 182, (2004), pp.181-192. (preprint: ECCC

  • J.Krajicek, A form of feasible interpolation for constant depth Frege systems , J. of Symbolic Logic, 75(2), (2010), pp. 774-784. Pdf file.

  • J.Krajicek a P.Pudlak: Some consequences of cryptographical conjectures for $S^1_2$ and $EF$", Information and Computation, Vol.140(1), (1998), pp.82-94.

  • P. Pudlak: Lower bounds for resolution and cutting planes proofs and monotone computations, J. of Symb. Logic 62(3), 1997, pp.981-998.

  • P.Pudlak: On reducibility and symmetry of disjoint NP-pairs, Theor.Comput.Science, 295, (2003), pp.323-339.

    References for Part 4 (will be updated significantly):

    My 2011 book (see above for a link) contains a survey of proof complexity generators in Chpts 29 and 30, as well as references to all papers on the topic. Below I list only those containing the material covered in the lectures.

  • M. Alekhnovich, E. Ben-Sasson, A.A.Razborov, and A. Wigderson, Pseudorandom Generators in Propositional Proof Complexity, SIAM Journal on Computing, Vol. 34(1) (2004) pp.67-88.

  • J.Krajicek, "On the weak pigeonhole principle", Fundamenta Mathematicae, Vol.170(1-3), (2001), pp.123-140.

  • J.Krajicek, Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds , J. of Symbolic Logic, 69(1), (2004), pp.265-286.

  • J.Krajicek, A proof complexity generator, in: Logic, Methodology and Philosophy of Science: Proc. of the 13th International Congress, Eds. Clark Glymour, Wei Wang, and Dag Westerstahl, College Publications, London, (2009), pp.185-190.
    ISBN-13: 978-1-904987-45-1. Pdf file.

  • J.Krajicek, On the proof complexity of the Nisan-Wigderson generator based on a hard NP \cap coNP function,
    J. of Mathematical Logic, Vol.11 (1), (2011), pp.11-27.

  • J.Pich, Circuit Lower Bounds in Bounded Arithmetics, Annals of Pure and Applied Logic, 166(1), 2015,

  • A.A.Razborov, Pseudorandom Generators Hard for k-DNF Resolution and Polynomial Calculus Resolution, Annals of Mathematics, Vol.181(2), (2015), pp.415-472.