__Proceedings article:__

** Pavel Pudlák and Samuel R. Buss.
"How To Lie Without Being (Easily) Convicted and Lengths of Proofs
in Propositional Calculus,"
**

** 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.**