Princeton University Computer Science Dept.

Computer Science 598g Advanced Topics in CS: Introduction to Proof Complexity   A. Razborov                     Literature

Spring 2000

    The following book (with a distinct logical flavour) covers many topics we will
study during our course:

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

    There are numerous textbooks on the mathematical logic, but it is not an
easy task to be entertaining when explaining the necessary technical machinery of
the subject. Still, the following two sources seems to have managed to keep the
amount of unaivodable boredom to the absolute minimum, and go on to interesting
things at a very reasonable speed:

    J. Shoenfield, Mathematical logic, Reading, Mass., Addison-Wesley Pub. Co.,
1967 (very advanced -- if you read it, then you basically know everything you
may want to know about the logic, or at least about the state of art in 1967);

    R. Lyndon, Notes on Logic, D. Van Nostrand Company, Princeton, New Jersey, 1966
(these are actually lecture notes. This amazing book is thin and when you read
it you have the feeling that nothing is happening, and at the end you realize that
you were taught, in some misterious way,  all basic facts from math logics...).

    I checked the last item out of library, but I will need it only occasionally
after Feb. 7. Please feel free to borrow it from me if you want to have a look!

    The following monograph (based on the PhD thesis defended at Princeton University
in 1985) is the seminal book which, to a certain extent, started off the whole
area of proofs in bounded arithmetic. Still, it is a very good (and very clearly written)
reading for the introductory level we are dealing with things in this course:

    S. Buss, Bounded Arithmetic, Bibliopolis, Napoli, 1986.

    The book

    P. Hajek, P. Pudlak, Metamathematics of First-Order Arithmetic, Springer-Verlag, 1993

is a rather advanced reading on fragments of Peano Arithmetic in general. The whole Chapter 5 is devoted to bounded arithemtic, and one can learn from it about practically all major results that have appeared since Buss's work.

    The same remark as above applies to these two books as well: I checked them out of library, but will need only occasionally after a couple of weeks. Feel free to borrow.

    One more source on bounded arithmetic that was just brought to my attention (and which, at the first glance, looks very sensible) are the first two chapters in the following book:

    Handbook of Proof Theory, Elsevier, 1998,

also written by S. Buss.

    There is no monograph yet specifically devoted to propositional proof complexity. Some material can be found in the above-cited sources on the theory of feasible proofs in general. You may also want to consult these surveys:

     A. Urquhart, The complexity of propositional proofs, Bulletin of Symbolic Logic, 1, 1995, 425-467.

     A. Razborov, Lower bounds for propositional proofs and independence results in Bounded Arithmetic, Proceedings of the 23rd ICALP, Lecture Notes in Computer Science 1099, 1996, 48-62.

     P. Beame and T. Pitassi, Propositional Proof Complexity: Past, Present and Future, ECCC, TR98-067.