DIMACS: Series in Discrete Mathematics and Theoretical Computer Science 1998; 320 pp; hardcover Volume: 39 ISBN10: 0821805770 ISBN13: 9780821805770 List Price: US$71 Member Price: US$56.80 Order Code: DIMACS/39
 Questions of mathematical proof and logical inference have been a significant thread in modern mathematics and have played a formative role in the development of computer science and artificial intelligence. Research in proof complexity and feasible theories of arithmetic aims at understanding not only whether logical inferences can be made, but also what resources are required to carry them out. Understanding the resources required for logical inferences has major implications for some of the most important problems in computational complexity, particularly the problem of whether NP is equal to coNP. In addition, these have important implications for the efficiency of automated reasoning systems. The last dozen years have seen several breakthroughs in the study of these resource requirements. Papers in this volume represent the proceedings of the DIMACS workshop on "Feasible Arithmetics and Proof Complexity" held in April 1996 at Rutgers University in New Jersey as part of the DIMACS Institute's Special Year on Logic and Algorithms. This book brings together some of the most recent work of leading researchers in proof complexity and feasible arithmetic reflecting many of these advances. It covers a number of aspects of the field, including lower bounds in proof complexity, witnessing theorems and proof systems for feasible arithmetic, algebraic and combinatorial proof systems, interpolation theorems, and the relationship between proof complexity and Boolean circuit complexity. Copublished with the Center for Discrete Mathematics and Theoretical Computer Science beginning with Volume 8. Volumes 17 were copublished with the Association for Computer Machinery (ACM). Readership Graduate students and research mathematicians interested in mathematical logic and foundations. Reviews "The volume adequately reflects current interests and trends in the area of feasible proofs, and many papers in it simply define the current state of the art there. Its importance for everybody interested in this beautiful theory, be it the experienced researcher, a beginner, or just a curious outsider, can hardly be overstated."  Journal of Symbolic Logic Table of Contents  J. Avigad  Plausibly hard combinatorial tautologies
 P. Beame and S. Riis  More on the relative strength of counting principles
 S. J. Bellantoni  Ranking arithmetic proofs by implicit ramification
 S. R. Buss  Lower bounds on Nullstellensatz proofs via designs
 S. Cook  Relating the provable collapse of \(\mathbf P\) to \(\mathrm {NC}^1\) and the power of logical theories
 P. Clote and A. Setzer  On \(PHP\), \(st\)connectivity, and odd charged graphs
 R. G. Downey, M. R. Fellows, and K. W. Regan  Descriptive complexity and the \(W\) hierarchy
 X. Fu  Lower bounds on the sizes of cutting plane proofs for modular coloring principles
 J. Johannsen  Equational calculi and constant depth propositional proofs
 S. Jukna  Exponential lower bounds for semantic resolution
 B. Kauffmann  Bounded arithmetic: Comparison of Buss' witnessing method and Sieg's Herbrand analysis
 A. Maciel and T. Pitassi  Towards lower bounds for boundeddepth Frege proofs with modular connectives
 F. Pitt  A quantifierfree theory based on a string algebra for \(NC^1\)
 C. Pollett  A propositional proof system for \(R^i_2\)
 P. Pudlák and J. Sgall  Algebraic models of computation and interpolation for algebraic proof systems
 D. E. Willard  Selfreflection principles and NPhardness
