Cut-elimination and Redundancy-elimination by Resolution

AbstractA new cut-elimination method for Gentzen’s LK is defined. First cut-elimination is generalized to the problem of redundancy-elimination. Then the elimination of redundancy in LK-proofs is performed by a resolution method in the following way. A set of clauses C is assigned to an LK-proof ψ and it is shown that C is always unsatisfiable. A resolution refutation of C then serves as a skeleton of an LK-proof ψ′ with atomic cuts;ψ′ can be constructed from the resolution proof and ψ by a projection method. In the final step the atomic cuts are eliminated and a cut-free proof is obtained. The complexity of the method is analyzed and it is shown that a non-elementary speed-up over Gentzen’s method can be achieved. Finally an application to automated deduction is presented: 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 be used to transform incorrect proofs into correct ones