This book presents an up-to-date, unified treatment of research in bounded arithmetic and
complexity of propositional logic with emphasis on independence proofs and lower bound …

§ 1. Introduction. The classical propositional calculus has an undeserved reputation among
logicians as being essentially trivial. I hope to convince the reader that it presents some of …

We prove lower bounds of the form exp (nε d), εd> 0, on the length of proofs of an explicit
sequence of tautologies, based on the Pigeonhole Principle, in proof systems using …

We consider small-weight Cutting Planes(CP*) proofs; that is, Cutting Planes(CP) proofs
with coefficients up to Poly (n). We use the well known lower bounds fc) r monotone …

It is generally conjectured that there is an exponential separation between Frege and
extended Frege systems. This paper reviews and introduces some candidates for families of …

We shall describe two general methods for proving lower bounds on the lengths of proofs in
propositional calculus and give examples of such lower bounds. One of the methods is …

We survey the best known lower bounds on symbols and lines in Frege and extended Frege
proofs. We prove that in minimum length sequent calculus proofs, no formula is generated …

The Hajós calculus is a simple, nondeterministic procedure that generates the class of non-3-
colorable graphs. Mansfield and Welsch posed the question of whether there exist graphs …

We propose a framework for proving lower bounds to the size of EF-proofs (equivalently, to
the number of proof-steps in F-proofs) in terms of boolean valuations. The concept is …

This paper discusses a claim made by Gödel in a letter to von Neumann which is closely
related to the P versus NP problem. Gödel's claim is that k-symbol provability in first-order …