The complexity of analytic tableaux. (English) Zbl 1109.03066

The paper settles the relative proof complexity of three variants of analytic tableaux, and tree resolution. Tree resolution was held for a long time to have exponential speed-up over analytic tableaux by a result of S. Cook and R. Reckhow [“On the lengths of proofs in the propositional calculus”, Proc. 6th ann. ACM Symp. Theory Comput., Seattle 1974, 135–148 (1974; Zbl 0375.02004)], until F. Massacci [Theor. Comput. Sci. 243, No. 1–2, 477–487 (2000; Zbl 0947.68130)] pointed out a gap in the proof, and constructed a quasi-polynomial tableaux refutation of their formulas.
In the present paper, the authors investigate the complexity of three variants of the tableau proof system: clausal tableaux, binary tableaux, and generalized clausal tableaux. It is shown that generalized clausal tableaux have an exponential speed-up over binary tableaux, and quasi-polynomially simulate tree resolution. The latter bound is tight, as the paper also provides a quasi-polynomial separation of tree resolution and generalized clausal tableaux. Together with the results of Cook and Reckhow, and Massacci (which imply an exponential speed-up of binary tableaux over clausal tableaux), this fully resolves the relative complexity of all the systems considered in the paper.


03F20 Complexity of proofs
Full Text: DOI


[1] Fibonacci Quarterly 11 pp 429– (1973)
[2] First-order logic (1968) · Zbl 0172.28901
[3] DOI: 10.2178/bsl/1203350879 · Zbl 1133.03037
[4] DOI: 10.1093/jigpal/2.2.205 · Zbl 0810.03008
[5] An exponential example for analytic tableaux (1973)
[6] 13th European Conference on Artificial Intelligence pp 408– (1998)
[7] Mathematics for the analysis of algorithms (1990)
[8] The relative efficiency of propositional proof systems 44 pp 36– (1979) · Zbl 0408.03044
[9] Proceedings of the Sixth Annual ACM Symposium on Theory of Computing 6 pp 15– (1974)
[10] DOI: 10.1016/S0304-3975(00)00148-1 · Zbl 0947.68130
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.