# zbMATH — the first resource for mathematics

Gentzen systems, resolution, and literal trees. (English) Zbl 0629.03038
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
Full Text: