Cut elimination and automatic proof procedures (Q1183598)

We first present a modified version of the cut elimination theorem and use an example to show that the upper bound (which is a function of the length of a proof and the complexity of the cut formulas in the proof) of the length of the cut-free proof given by the modified cut elimination theorem matches the length of the cut-free proof of the example. We also discuss the resolution method and some of its refinements with respect to the possibility of using cut. For each refinement, we give an upper bound (for the shortest cut-free proof) as a function of the length of the refutation. On the other hand, we give examples which show that the upper bounds are minimal. Finally, we discuss why the usual proof methods are cut-free.