2014/02/11 by Stefan Hetzl, Alexander Leitsch, Hetzl, Stefan +7
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1402.2474
openalex publication_date 2014/02/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 ∀ x.A (for quantifier-free A) to a method generating lemmas of the form ∀ x1…∀ xn.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.