Journal article:

Samuel R. Buss.
"Some remarks on the lengths of propositional proofs."
Archive for Mathematical Logic 34 (1995) 377-394.

Download article: postscript or PDF

From the introduction: This paper considers the lengths of proofs of propositional tautologies; we measure proof length either by counting the number of lines (formulas) in the proof or by counting the number of symbols in the proof.

The first three sections give lower bounds on proof lengths which are quite easy to obtain and yet represent the best currently-known lower bounds. The contents of sections 1-3 have already appeared in prior work, but they are fundamental and are not widely known, so we feel it is useful to exposite them here. This author first discovered the results of sections 2 and 3 from considering the logical-flow graph~\cite{Buss:kprove}; however, the proofs presented in this paper are much simpler. Other prior work with results similar to the contents of sections 2 and 3 includes Cejtin-\v Cubarjan\cite{CejtinCubarjan:somebounds}, Buss-et~al.~\cite{Bussetal:Math271}, Kraj\'\i\v cek~\cite{Krajicek:propositionalspeedup,Krajicek:number}, Bonet~\cite{Bonet:symbollength}, Bonet-Buss~\cite{BonetBuss:deduction}, and Buss~\cite{Buss:godeltwo}.

In section 4, we define a new version $PK$ of the propositional sequent calculus and pose the problem of finding a $(1+\epsilon)n$ lower bound on the size of $PK$-proofs. We give the currently best known lower bound of $n+\Omega(n^{1/3})$.

In section 5, it is shown that in minimum length tree-like $PK$-proofs, no formula is introduced twice as a conclusion or used twice as a hypothesis on any single branch in the proof.

In section 6, we discuss the open problem of whether cycles can eliminated from the logical flow graph of a proof without a superpolynomial size penalty.

In section 7, we prove a new result showing the equivalence of constant-depth Frege proofs with polynomially many lines and constant-depth Frege proofs with polynomially many symbols.

In section 8, we prove that the variable renaming inference rule is unexpectedly powerful, in that renaming Frege proof systems are p-equivalent to extended Frege proof systems.

Back to Sam Buss's publications page.