Proof Complexity

Offers a self-contained work presenting basic ideas, classical results, current state of the art and possible future directions in proof complexity.

Jan Krají?ek (Author)

9781108416849, Cambridge University Press

Hardback, published 28 March 2019

530 pages
24.1 x 16.1 x 3.3 cm, 0.91 kg

'This book is in my view an excellent reference manual for a fundamental topic in mathematical logic and theoretical computer science.' Jaap van Oosten, Boekbesprekingen

Proof complexity is a rich subject drawing on methods from logic, combinatorics, algebra and computer science. This self-contained book presents the basic concepts, classical results, current state of the art and possible future directions in the field. It stresses a view of proof complexity as a whole entity rather than a collection of various topics held together loosely by a few notions, and it favors more generalizable statements. Lower bounds for lengths of proofs, often regarded as the key issue in proof complexity, are of course covered in detail. However, upper bounds are not neglected: this book also explores the relations between bounded arithmetic theories and proof systems and how they can be used to prove upper bounds on lengths of proofs and simulations among proof systems. It goes on to discuss topics that transcend specific proof systems, allowing for deeper understanding of the fundamental problems of the subject.

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.

Subject Areas: Artificial intelligence [UYQ], Maths for computer scientists [UYAM], Mathematical logic [PBCD]