Cut-elimination and redundancy-elimination by resolution

A new cut-elimination method for Gentzen's LK is defined. First cut-elimina tion is generalized to the problem of redundancy-elimination. Then the elim ination of redundancy in LK-proofs is performed by a resolution method in t he following way. A set of clauses C is assigned to an LK-proof psi and it is shown that C is always unsatisfiable. A resolution refutation of C then serves as a skeleton of an LK-proof psi' with atomic cuts. psi' can be cons tructed from the resolution proof and psi by a projection method. In the fi nal step the atomic cuts are eliminated and a cut-free proof is obtained. T he complexity of the method is analyzed and it is shown that a non-elementa ry speed-up over Gentzen's method can be achieved. Finally an application t o automated deduction is I,resented: it is demonstrated how informal proofs (containing pseudo-cuts) can be transformed into formal ones by the method of redundancy-elimination; moreover, the method can even he used to transf orm incorrect proofs into correct ones. (C) 2000 Academic Press.