Introducing Quantified Cuts in Logic with Equality

Stefan Hetzl, Alexander Leitsch, Giselle Reis +2

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…