Logical Foundations of Proof Complexity

By: Stephen Cook, Phuong Nguyen

Write A Review

Hardcover | 25 January 2010

At a Glance

Hardcover
496 Pages

Dimensions(cm)
23.39 x 15.6 x 3.18

Hardcover

RRP $209.95

$184.75

12%OFF

or 4 interest-free payments of $46.19 with

or

Ships in 5 to 7 business days

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.

Industry Reviews

'The book under review is a comprehensive introduction to bounded arithmetic ... While the book is primarily aimed at students and researchers with background in theoretical computer science, its prerequisites in computational complexity are rather mild and are summarized in the Appendix, thus the book should be easily accessible to logicians and mathematicians coming from a different background. Some familiarity with logic will help the reader, but in this respect the book is more or less self-contained, the relevant bits of proof theory and model theory are developed in the first chapters in detail.' Zentralblatt MATH

Shipping

	Standard Shipping	Express Shipping
Metro postcodes:	$9.99	$14.95
Regional postcodes:	$9.99	$14.95
Rural postcodes:	$9.99	$14.95

Orders over $79.00 qualify for free shipping.

How to return your order

At Booktopia, we offer hassle-free returns in accordance with our returns policy. If you wish to return an item, please get in touch with Booktopia Customer Care.

Additional postage charges may be applicable.

Defective items

If there is a problem with any of the items received for your order then the Booktopia Customer Care team is ready to assist you.

For more info please visit our Help Centre.

More in Mathematical Logic

Current Trends in Automated Reasoning - Erika Bach

$31.75

21%
OFF

The Language of Mathematics

The Stories behind the Symbols

Hardcover

RRP $49.99

$40.75

18%
OFF

Introduction to Modern Cryptography : Revised Third Edition - Jonathan Katz

$85.75

10%
OFF

Cryptocurrency Forensics and Investigation using Open Source Intelligence Techniques (OSINT)

Volume I

Hardcover

RRP $231.00

$202.75

12%
OFF

Essays in Analysis : Routledge Revivals - Alice Ambrose

$233.75

Mathematical Puzzles

Revised Edition

Paperback

RRP $56.99

$52.75

Lectures on the Philosophy of Mathematics - Joel David Hamkins

$137.75

25%
OFF

Strongly Minimal Sets and Categoricity in Continuous Logic

Paperback

RRP $197.00

$187.75

Preface	p. xiii
Introduction	p. 1
The Predicate Calculus and the System LK	p. 9
Propositional Calculus	p. 9
Gentzen's Propositional Proof System PK	p. 10
Soundness and Completeness of PK	p. 12
PK Proofs from Assumptions	p. 13
Propositional Compactness	p. 16
Predicate Calculus	p. 17
Syntax of the Predicate Calculus	p. 17
Semantics of Predicate Calculus	p. 19
The First-Order Proof System LK	p. 21
Free Variable Normal Form	p. 23
Completeness of LK without Equality	p. 24
Equality Axioms	p. 31
Equality Axioms for LK	p. 32
Revised Soundness and Completeness of LK	p. 33
Major Corollaries of Completeness	p. 34
The Herbrand Theorem	p. 35
Notes	p. 38
Peano Arithmetic and Its Subsystems	p. 39
Peano Arithmetic	p. 39
Minimization	p. 44
Bounded Induction Scheme	p. 44
Strong Induction Scheme	p. 44
Parikh's Theorem	p. 44
Conservative Extensions of I₀	p. 49
Introducing New Function and Predicate Symbols	p. 50
<$$$>: A Universal Conservative Extension of I₀	p. 54
Defining y = 2^x and BIT(i, x) in I₀	p. 59
I₀ and the Linear Time Hierarchy	p. 65
The Polynomial and Linear Time Hierarchies	p. 65
Representability of LTH Relations	p. 66
Characterizing the LTH by I₀	p. 69
Buss's Sⁱ₂; Hierarchy: The Road Not Taken	p. 70
Notes	p. 71
Two-Sorted Logic and Complexity Classes	p. 73
Basic Descriptive Complexity Theory	p. 74
Two-Sorted First-Order Logic	p. 76
Syntax	p. 76
Semantics	p. 78
Two-Sorted Complexity Classes	p. 80
Notation for Numbers and Finite Sets	p. 80
Representation Theorems	p. 81
The LTH Revisited	p. 86
The Proof System LK²	p. 87
Two-Sorted Free Variable Normal Form	p. 90
Single-Sorted Logic Interpretation	p. 91
Notes	p. 93
The Theory V⁰ and AC⁰	p. 95
Definition and Basic Properties0 of Vⁱ	p. 95
Two-Sorted Functions	p. 101
Parikh's Theorem for Two-Sorted Logic	p. 104
Definability in V⁰	p. 106
¹₁-Definable Predicates	p. 115
The Witnessing Theorem for V⁰	p. 117
Independence Follows from the Witnessing Theorem for V⁰	p. 118
Proof of the Witnessing Theorem for V⁰	p. 119
<$$$>: Universal Conservative Extension of V⁰	p. 124
Alternative Proof of the Witnessing Theorem for V⁰	p. 127
Finite Axiomatizability	p. 129
Notes	p. 130
The Theory V¹ and Polynomial Time	p. 133
Induction Schemes in Vⁱ	p. 133
Characterizing P by V¹	p. 135
The "If" Direction of Theorem VI.2.2.	p. 137
Application of Cobham's Theorem	p. 140
The Replacement Axiom Scheme	p. 142
Extending V¹ by Polytime Functions	p. 145
The Witnessing Theorem for V¹	p. 147
The Sequent System LK²-<$$$>	p. 150
Proof of the Witnessing Theorem for V¹	p. 154
Notes	p. 156
Propositional Translations	p. 159
Propositional Proof Systems	p. 160
Treelike vs Daglike Proof Systems	p. 162
The Pigeonhole Principle and Bounded Depth PK	p. 163
Translating V⁰ to bPK	p. 165
Translating ^B₀ Formulas	p. 166
<$$$> and LK²-<$$$>	p. 169
Proof of the Translation Theorem for V⁰	p. 170
Quantified Propositional Calculus	p. 173
QPC Proof Systems	p. 175
The System G	p. 175
The Systems G₀ and G^*_i	p. 179
Extended Frege Systems and Witnessing in G^*₁	p. 186
Propositional Translations for Vⁱ	p. 191
Translating V⁰ to Bounded Depth G^*₀	p. 195
Notes	p. 198
Theories for Polynomial Time and Beyond	p. 201
The Theory VP and Aggregate Functions	p. 201
The Theory <$$$>	p. 207
The Theory VPV	p. 210
Comparing VPV and V¹	p. 213
VPV Is Conservative over VP	p. 214
TV⁰ and the TVⁱ Hierarchy	p. 217
TV⁰ ⊆ VPV	p. 220
Bit Recursion	p. 222
The Theory V¹-HORN	p. 223
TV¹ and Polynomial Local Search	p. 228
KPT Witnessing and Replacement	p. 237
Applying KPT Witnessing	p. 239
More on Vⁱ and TVⁱ	p. 243
Finite Axiomatizability	p. 243
Definability in the V^? Hierarchy	p. 245
Collapse of V^? vs Collapse of PH	p. 253
RSUV Isomorphism	p. 256
The Theories Sⁱ₂ and Tⁱ₂	p. 256
RSUV Isomorphism	p. 258
The # Translation	p. 260
The b Translation	p. 262
The RSUV Isomorphism between Sⁱ₂ and Vⁱ	p. 263
Notes	p. 266
Theories for Small Classes	p. 267
AC⁰ Reductions	p. 269
Theories for Subclasses of P	p. 272
The Theories VC	p. 273
The Theory <$$$>	p. 274
The Theory <$$$>	p. 278
Obtaining Theories for the Classes of Interest	p. 280
Theories for TC⁰	p. 281
The Class TC⁰	p. 282
The Theories VTC⁰, <$$$>, and <$$$>	p. 283
Number Recursion and Number Summation	p. 287
The Theory VTC⁰V	p. 289
Proving the Pigeonhole Principle in VTC⁰	p. 291
Denning String Multiplication in VTC⁰	p. 293
Proving Finite Szpilrajn's Theorem in VTC⁰	p. 298
Proving Bondy's Theorem	p. 299
Theories for AC⁰ (m) and ACC	p. 303
The Classes AC⁰ (m) and ACC	p. 303
The Theories V⁰(2), <$$$>, and <$$$>	p. 304
The "onto" PHP and Parity Principle	p. 306
The Theory VAC⁰ (2)V	p. 308
The Jordan Curve Theorem and Related Principles	p. 309
The Theories for AC⁰ (m) and ACC	p. 313
The Modulo m Counting Principles	p. 316
The Theory VAC⁰ (6)V	p. 318
Theories for NC¹ and the NC Hierarchy	p. 319
Definitions of the Classes	p. 320
BSVP and NC¹	p. 321
The Theories VNC¹, <$$$>, and <$$$>	p. 323
VTC⁰ ⊆ VNC¹	p. 326
The Theory VNC¹ V	p. 333
Theories for the NC Hierarchy	p. 335
Theories for NL and L	p. 339
The Theories VNL, <$$$>, and <$$$>	p. 339
The Theory V¹-KROM	p. 343
The Theories VL, <$$$>, and <$$$>	p. 351
The Theory VLV	p. 356
Open Problems	p. 358
Proving Cayley-Hamilton in VNC²	p. 358
VSL and VSL <$$$> VL	p. 358
Denning [X/Y] in VTC⁰	p. 360
Proving PHP and Count_m′ in V⁰ (m)	p. 360
Notes	p. 360
Proof Systems and the Reflection Principle	p. 363
Formalizing Propositional Translations	p. 364
Verifying Proofs in TC⁰	p. 364
Computing Propositional Translations in TC⁰	p. 373
The Propositional Translation Theorem for TVⁱ	p. 377
The Reflection Principle	p. 382
Truth Definitions	p. 383
Truth Definitions vs Propositional Translations	p. 387
RFN and Consistency for Subsystems of G	p. 396
Axiomatizations Using RFN	p. 403
Proving -Simulations Using RFN	p. 407
The Witnessing Problems for G	p. 408
VNC¹ and G^*₀	p. 410
Propositional Translation for VNC¹	p. 410
The Boolean Sentence Value Problem	p. 414
Reflection Principle for PK	p. 421
VTC⁰ and Threshold Logic	p. 428
The Sequent Calculus PTK	p. 428
Reflection Principles for Bounded Depth PTK	p. 433
Propositional Translation for VTC⁰	p. 434
Bounded Depth GTC⁰	p. 441
Notes	p. 442
Computation Models	p. 445
Deterministic Turing Machines	p. 445
L, P, PSPACE, and EXP	p. 447
Nondeterministic Turing Machines	p. 449
Oracle Turing Machines	p. 451
Alternating Turing Machines	p. 452
Uniform Circuit Families	p. 453
Bibliography	p. 457
Index	p. 465
Table of Contents provided by Ingram. All Rights Reserved.

Logical Foundations of Proof Complexity

At a Glance

Hardcover

Industry Reviews

Shipping

How to return your order

Defective items

You Can Find This Book In

More in Mathematical Logic

Current Trends in Automated Reasoning

Automated Theorem Proving

Theory and Practice

Handbook of Automated Reasoning

Current Trends in Automated Theorem Proving

Automated Deduction

From Theory to Applications

Advances in Automated Reasoning

Unequal

The Maths of When Things Do and Don't Add Up

The Language of Mathematics

The Stories behind the Symbols

Introduction to Modern Cryptography

Revised Third Edition

Introduction to Mathematical Logic

Discrete Mathematics and Its Applications

The Equation of Knowledge

From Bayes' Rule to a Unified Philosophy of Science

Cryptocurrency Forensics and Investigation using Open Source Intelligence Techniques (OSINT)

Volume I

Cryptocurrency Forensics and Investigation using Open Source Intelligence Techniques (OSINT)

Volume I

Essays in Analysis

Routledge Revivals

Fuzzy Logic in Revolutionizing Renewable Energy

Jenny Stanford Series on Fuzzy Theory Frontiers Vol. 2

Introduction to Modern Cryptography

Chapman & Hall/Crc Cryptography and Network Security

Mathematical Puzzles

Revised Edition

Lectures on the Philosophy of Mathematics

Ignorance

What We Do Not Know, Cannot Know, Must Not Know, and Refuse to Know

Cause, Effect, and Everything in Between

An Introduction to Causal Inference

Strongly Minimal Sets and Categoricity in Continuous Logic

The Times Fiendish Su Doku Book 19

200 Challenging Su Doku Puzzles

The Times Ultimate Killer Su Doku Book 18

200 of the Deadliest Su Doku Puzzles

Reading, Writing, and Proving

A Closer Look at Mathematics

This product is categorised by