Samuel R. Buss.
"Propositional consistency proofs."
Annals of Pure and Applied Logic 52 (1991) 3-29.
Download article: postscript or PDF.
Abstract: Partial consistency statements can be
expressed as polynomial-size propositional formulas. Frege proof systems have
polynomial-size partial self-consistency proofs. Frege proof systems have polynomial-size
proofs of partial consistency of extended Frege proof systems if and only if Frege proof
systems polynomially simulate extended Frege proof systems. We give a new proof of
Reckhow's theorem that any two Frege proof systems p-simulate each other.
The proofs depend on polynomial size propositional formulas defining the truth of propositional formulas. These are already known to exist since the Boolean formula value problem is in alternating logarithmic time; this paper presents a proof of this fact based on a construction which is somewhat simpler than the prior proofs of Buss and of Buss-Cook-Gupta-Ramachandran.
Back to Sam Buss's publications page.