Pavel Pudlák and Samuel R. Buss.
"How To Lie Without Being (Easily) Convicted and Lengths of Proofs in Propositional Calculus,"
In Eighth Workshop on Computer Science Logic (CSL'94),
Lecture Notes in Computer Science #933, 1995, Springer-Verlag, pp. 151-162.
Abstract: 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 based on interactive proofs where one player is claiming that he has a falsifying assignment for a tautology and the second player is trying to convict him of a lie. The second method is based on boolean valuations. For the first method, a $\log n +\log\log n -O(\log\log\log n)$ lower bound is given on the lengths of interactive proofs of certain permutation tautologies.
Download postscript or PDF.
Back to Sam Buss's publications page.