Introducing Quantified Cuts in Logic with Equality

TL;DR

This paper extends a proof structuring technique called cut-introduction to handle quantified lemmas with multiple quantifiers and equality in predicate logic, improving its effectiveness and applicability.

Contribution

The paper introduces a generalized cut-introduction method for multiple quantifiers and equality, with implementation and empirical evaluation on a proof database.

Findings

Significant improvement over previous algorithms.

Effective handling of equality in proof compression.

Successful application to a large proof database.

Abstract

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.