Logical Foundations of Proof Complexity
Logical Foundations of Proof Complexity
This book treats bounded arithmetic and propositional proof complexity from the point of view of computational complexity. The first seven chapters include the necessary logical background for the material and are suitable for a graduate course. Associated with each of many complexity classes are both a two-sorted predicate calculus theory, with induction restricted to concepts in the class, and a propositional proof system. The complexity classes range from AC0 for the weakest theory up to the polynomial hierarchy. Each bounded theorem in a theory translates into a family of (quantified) propositional tautologies with polynomial size proofs in the corresponding proof system. The theory proves the soundness of the associated proof system. The result is a uniform treatment of many systems in the literature, including Buss's theories for the polynomial hierarchy and many disparate systems for complexity classes such as AC0, AC0(m), TC0, NC1, L, NL, NC, and P.
- Suitable as an advanced graduate text
- Contains a wealth of original material
- Will serve as a valuable reference for proof complexity
Reviews & endorsements
"This authoritative volume on computational complexity of logical systems provides a sound background in logic for computer science and mathematics students. The book provides a number of exercises that offer insights into the presented material and facilitate the understanding of the concepts and results. The list of bibliographic references contains the most-representative published work in the domains of proof and computational complexity theories."
L. State, reviews.com
"This most erudite of books will stand the test of time. I will revisit it often."
George Hacken, Computing Reviews
"... very great detail and with care... The presentation of the book is most thorough and the treatment rigorous, providing the reader with the right amount of intuition and detail to follow even complicated constructions. The new book by Cook and Nguyen will become another classic for the field of bounded arithmetic and its relations to computational complexity and propositional proof complexity. It will serve as a rich source of reference for the expert and as a thorough guide to the student interested in learning about this beautiful field."
Olaf Beyersdorff, Mathematical Reviews
Product details
June 2014Paperback
9781107694118
496 pages
234 × 156 × 28 mm
0.76kg
17 b/w illus. 5 tables
Available
Table of Contents
- 1. Introduction
- 2. The predicate calculus and the system
- 3. Peano arithmetic and its subsystems
- 4. Two-sorted logic and complexity classes
- 5. The theory V0 and AC0
- 6. The theory V1 and polynomial time
- 7. Propositional translations
- 8. Theories for polynomial time and beyond
- 9. Theories for small classes
- 10. Proof systems and the reflection principle
- 11. Computation models.
