引入等式逻辑中的量化割
Introducing Quantified Cuts in Logic with Equality
摘要：
割引入是一种构造和压缩形式证明的技术。在本文中，我们推广我们的削减引进方法的形式$\forall x.A$（无量词$A$）的量化引理的方法生成引理的形式$\forall x_1\ldots\forall x_n.A$。此外，我们将原来的方法扩展到谓词逻辑与平等。该方法已在TSTP证明数据库中得到实现和应用。结果表明，该方法的扩展，以处理平等和量化器块导致一个大幅度的改进旧算法。
英文摘要：
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 $\forall x.A$ (for quantifier-free $A$) to a method generating lemmas of the form $\forall x_1\ldots\forall 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
