Proof Complexity

Jan Krajíček is Professor of Mathematical Logic in the Faculty of Mathematics and Physics at Charles University, Prague. He is a member of the Academia Europaea and of the Learned Society of the Czech Republic. He has been an invited speaker at the European Congress of Mathematicians and at the International Congresses of Logic, Methodology and Philosophy of Science.

• Introduction; Part I. Basic Concepts: 1. Concepts and problems; 2. Frege systems; 3. Sequent calculus; 4. Quantified propositional calculus; 5. Resolution; 6. Algebraic and geometric proof systems; 7. Further proof systems; Part II. Upper Bounds: 8. Basic example of the correspondence between theories and proof systems; 9. Two worlds of bounded arithmetic; 10. Up to EF via the <...> translation; 11. Examples of upper bounds and p-simulations; 12. Beyond EF via the || ... || translation; Part III. Lower Bounds: 13. R and R-like proof systems; 14. {LK}_{d + 1/2} and combinatorial restrictions; 15. F_d and logical restrictions; 16. Algebraic and geometric proof systems; 17. Feasible interpolation: a framework; 18. Feasible interpolation: applications; Part IV. Beyond Bounds: 19. Hard tautologies; 20. Model theory and lower bounds; 21. Optimality; 22. The nature of proof complexity; Bibliography; Special symbols; Index.

'… the book has very rich content and its bibliographical material includes all previous books and survey articles related to proof complexity.' Anahit Artashes Chubaryan, MathSciNet