Dougherty, Daniel J. Gentzen systems, resolution, and literal trees. (English) Zbl 0629.03038 Notre Dame J. Formal Logic 27, 483-503 (1986). The paper deals with the length of proofs in various calculi for propositional logic, in particular Gentzen’s sequential calculus and the resolution method. The method employed here uses transformations between proofs in the various systems. In particular, the author exhibits a sequential calculus \(G_ 1\) with cut whose proofs correspond exactly to the derivations in the resolution calculus. From the complexity results we mention that the system \(G_ 1\) is not a polynomially bounded proof system. Other results deal with extended resolution and cut elimination; of particular interest is that eliminating cuts never substantially shortens the proofs. Reviewer: M.M.Richter MSC: 03F20 Complexity of proofs 03F15 Recursive ordinals and ordinal notations 03F05 Cut-elimination and normal-form theorems 03B35 Mechanization of proofs and logical operations Keywords:length of proofs; calculi for propositional logic; Gentzen’s sequential calculus; resolution; extended resolution; cut elimination PDF BibTeX XML Cite \textit{D. J. Dougherty}, Notre Dame J. Formal Logic 27, 483--503 (1986; Zbl 0629.03038) Full Text: DOI