The proof complexity of analytic and clausal tableaux

DOI10.1016/S0304-3975(00)00148-1MaRDI QIDQ1575658zbMATH OpenOpenAlexWikidataFDO

Authors Fabio Massacci

Publication date 21 August 2000

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0304-3975(00)00148-1

zbMATH Keywords

analytic tableauxautomated reasoningclausal tableauxproof complexitytree resolution

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Review text

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.

Recommendations

• The complexity of analytic tableaux
• The complexity of analytic tableaux
• Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
• On the Computational Intractability of Analytic Tableau Methods

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A proper hierarchy of propositional sequent calculi
• Controlled integration of the cut rule into connection tableau calculi
• scientific article; zbMATH DE number 3583767 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• Hyper tableaux
• Mechanical Theorem-Proving by Model Elimination
• On the Computational Intractability of Analytic Tableau Methods
• On the relative merits of path dissolution and the method of analytic tableaux
• The Complexity of Propositional Proofs
• The relative efficiency of propositional proof systems
• The Taming of the Cut. Classical Refutations with Analytic Cut

Cited in

(9)

• Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
• Accelerating tableaux proofs using compact representations
• The expected complexity of analytic tableaux analyses in propositional calculus. II
• A tableaux calculus for reducing proof size
• A bibliography on analytic tableaux theorem proving
• The complexity of analytic tableaux
• BDD-based decision procedures for the modal logic K ★
• The complexity of analytic tableaux
• The relative complexity of analytic tableaux and SL-resolution

This page was built for publication: The proof complexity of analytic and clausal tableaux

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1575658)