Introducing Quantified Cuts in Logic with Equality.

Cut-introduction is a technique for structuring and compressing formal proofs. In this paper we generalize our cut-introduction method for the introduction of quantified lemmas of the form for all x.A (for quantifier-free A) to a method generating lemmas of the form for all x(1) ... for all x(n).A. Moreover, we extend the original method to predicate logic with equality. The new method was implemented and applied to the TSTP proof database. It is shown that the extension of the method to handle equality and quantifier-blocks leads to a substantial improvement of the old algorithm.