The proof complexity of analytic and clausal tableaux (Q1575658): Difference between revisions
From MaRDI portal
Latest revision as of 16:58, 31 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | The proof complexity of analytic and clausal tableaux |
scientific article |
Statements
The proof complexity of analytic and clausal tableaux (English)
0 references
21 August 2000
0 references
It is widely believed that a family \(\Sigma_{n}\) of unsatisfiable formulae proposed by \textit{S. Cook} and \textit{R. Reckhow} in their landmark paper [Proc. 6th ann. ACM Symp. Theory Comput., Seattle 1974, 135-148 (1974; Zbl 0375.02004)] can be used to give a lower bound of \(2^{\Omega(2^{n})}\) 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 \(\Sigma_{n}\) for whose size we prove an upper bound of \(O(2^{n^{2}})\), 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.
0 references
analytic tableaux
0 references
automated reasoning
0 references
clausal tableaux
0 references
proof complexity
0 references
tree resolution
0 references