It is widely believed that a family ∑ n of unsatisfiable formulae proposed by Cook and Reckhow in their landmark paper (Proc. ACM Symp. on Theory of Computing, 1974) can be used to give a lower bound of 2 Ω(2n) on the proof size with analytic tableaux. This claim plays a key role in the proof that tableaux cannot polynomially simulate tree resolution. We exhibit an analytic tableau proof for ∑ n for whose size we prove an upper bound of O(2 n2 ), which, although not polynomial in the size O(2 n ) of the input formula, is exponentially shorter than the claimed lower bound. An analysis of the proofs published in the literature reveals that the pitfall is the blurring of n-ary (clausal) and binary versions of tableaux. A consequence of this analysis is that a second widely held belief falls too: clausal tableaux are not just a more efficient notational variant of analytic tableaux for formulae in clausal normal form. Indeed clausal tableaux (and thus model elimination without lemmaizing) cannot polynomially simulate analytic tableaux. © 2000 Elsevier Science B.V. All rights reserved.
Massacci, F. (2000). The proof complexity of analytic and clausal tableaux. Theoretical Computer Science, 243(1–2), 477–487. https://doi.org/10.1016/S0304-3975(00)00148-1