The proof complexity of analytic and clausal tableaux

Citations of this article
Mendeley users who have this article in their library.


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.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free