Gentzen systems, resolution, and literal trees (Q1093632)

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.