Discrete Mathematics and Theoretical Computer Science

TITLE: "Proof Complexity and Feasible Arithmetics"

EDITOR: P. Beam and S. Buss.

Published by the American Mathematical Society

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 ofPtoNCand the power of logical theories Stephen Cook 73 On^{1}PHP st-connectivity, and odd charged graphs Peter Clote and Anton Setzer 93 Descriptive complexity and theWhierarchy 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 forNC^{1}François Pitt 229 A propositional proof system forRChris 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^{i}_{2}

Index of Volumes

DIMACS Homepage

Contacting the Center

Document last modified on October 28, 1998.