DIMACS Series in
Discrete Mathematics and Theoretical Computer Science

VOLUME Thirty Nine
TITLE: "Proof Complexity and Feasible Arithmetics"
EDITOR: P. Beam and S. Buss.
Published by the American Mathematical Society

Ordering Information

This volume may be obtained from the AMS or through bookstores in your area.

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 Index of Volumes
DIMACS Homepage
Contacting the Center
Document last modified on October 28, 1998.