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
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: DOI