To order through AMS contact the AMS Customer Services Department, P.O. Box 6248, Providence, Rhode Island 02940-6248 USA. For Visa, Mastercard, Discover, and American Express orders call 1-800-321-4AMS.
You may also visit the AMS Bookstore and order directly from there. DIMACS does not distribute or sell these books.
The complexity of proofs in propositional logic and the properties of feasible theories of arithmetic are closely related and give important and strong connections between logical properties and the properties of computational complexity classes.
Defining the proof complexity of logical formulas requires the specification of a particular proof system that determines the expressive power of and the relationships between the objects that may be used in their proofs. In addition, a proof system includes an efficient mechanism for checking the validity of proofs. Within such a proof system, the proof complexity of a formula is typically measured as the amount of space required to write down a proof. The study of proof complexity seeks to understand the complexity of proofs of formulas in specific proof systems, classify the relative complexity of proofs of formulas within different proof systems, and to develop better proof systems. For example, a major open question in proof complexity, equivalent to the NP versus co-NP problem, is whether or not there is a proof system in which all propositional tautologies have polynomial-size proofs.
Feasible theories of arithmetic are first-order theories of arithmetic designed to have proof-theoretic strength closely corresponding to low-level computational classes from the polynomial-time or NC hierarchies. The most natural feasible theories of arithmetic have the property that the functions which are provably total in the theory are precisely the functions which are computable is some give natural complexity class. Furthermore, it is frequently the case that first-order proofs in feasible theories of arithmetic can be translated directly into propositional proofs. The primary goals of the study of feasible theories of arithmetic are to understand the computational implications of various proof-theoretic constructions and use these to characterize complexity classes, and to establish connections between the logical properties of feasible theories and open problems in computational complexity. It is hoped that the study of feasible theories will ultimately yield useful new complexity results.
Over the last dozen years there has been substantial progress in proof complexity and feasible arithmetic as the two have grown together and have also benefited from a very productive cross-fertilization of techniques with Boolean circuit complexity. This progress has significantly broadened and deepened many connections of proof complexity and feasible arithmetic with computational complexity and greatly enriched both areas.
The papers in this volume represent the proceedings of workshop on ``Feasible Arithmetic and Proof Complexity'' held at the DIMACS Institute at Rutgers, New Jersey on April 21-24, 1996. The principal speakers at this workshop included J. Avigad, P. Beame, S. Bellantoni, S. Buss, J.-Y. Cai, A. Carbone, P. Clote, F. Ferreira, X. Fu, R. Impagliazzo, J. Johannsen, B. Kauffmann, J. Kraj\'\i\v cek, D. Leivant, A.A. Razborov, K. Regan, S. Riis, T. Pitassi, P. Pudlak, S. Rudich, G. Takeuti and D. Willard, and many of these speakers submitted talks to this volume. The papers primarily cover lower bounds on the complexity of propositional proofs and meta-mathematical results on feasible theories of arithmetics. All papers in this volume are refereed.
We wish to thank the DIMACS institute for their generous support in hosting and financing the workshop and the DIMACS staff for their help in organizing the meeting. We also thank the referees for the rigorous and thorough review of the articles.
Paul Beame and Sam Buss
Plausibly hard combinatorial tautologies
Jeremy Avigad 1
More on the relative strength of counting principles
Paul Beame and Søren Riis 13
Ranking arithmetic proofs by implicit ramification
Stephen J. Bellantoni 37
Lower bounds on Nullstellensatz proofs via designs
Samuel R. Buss 59
Relating the provable collapse of P to NC1 and the power
of logical theories
Stephen Cook 73
On PHP st-connectivity, and odd charged graphs
Peter Clote and Anton Setzer 93
Descriptive complexity and the W hierarchy
Rodney G. Downey, Michael R. Fellows and Kenneth W. Regan 119
Lower bounds on sizes of cutting plane proofs for modular
coloring principles
Xudong Fu 135
Equational calculi and constant depth propositional proofs
Jan Johannsen 149
Exponential lower bounds for semantic resolution
Stasys Jukna 163
Bounded arithmetic: Comparison of Buss' witnessing method
and Sieg's Herbrand analysis
Barbara Kauffmann 173
Towards lower bounds for bounded-depth Frege proofs with
modular connectives
Alexis Maciel and Toniann Pitassi 195
A quantifier-free theory based on a string algebra for NC1
François Pitt 229
A propositional proof system for Ri2
Chris Pollett 253
Algebraic models of computation and interpolation for
algebraic proof systems
Pavel Pudlák and Jirí Sgall 279
Self-reflection principles and NP-hardness
Dan E. Willard 297
Index of Volumes
DIMACS Homepage