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 ∀xA (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. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Hetzl, S., Leitsch, A., Reis, G., Tapolczai, J., & Weller, D. (2014). Introducing quantified cuts in logic with equality. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8562 LNAI, pp. 240–254). Springer Verlag. https://doi.org/10.1007/978-3-319-08587-6_17
Mendeley helps you to discover research relevant for your work.