Splitting Proofs for Interpolation

TL;DR

This paper introduces a novel approach to extracting interpolants from local first-order refutations by separating logical strength conditions and common signature requirements, resulting in an efficient algorithm that improves first-order interpolation.

Contribution

The paper presents a new theoretical perspective and an efficient algorithm for interpolant extraction that is linear in refutation size and optimizable by various metrics.

Findings

Algorithm is linear in refutation size.

Implementation in VAMPIRE shows improved performance.

Practical evaluation demonstrates state-of-the-art results.

Abstract

We study interpolant extraction from local first-order refutations. We present a new theoretical perspective on interpolation based on clearly separating the condition on logical strength of the formula from the requirement on the com- mon signature. This allows us to highlight the space of all interpolants that can be extracted from a refutation as a space of simple choices on how to split the refuta- tion into two parts. We use this new insight to develop an algorithm for extracting interpolants which are linear in the size of the input refutation and can be further optimized using metrics such as number of non-logical symbols or quantifiers. We implemented the new algorithm in first-order theorem prover VAMPIRE and evaluated it on a large number of examples coming from the first-order proving community. Our experiments give practical evidence that our work improves the state-of-the-art in first-order interpolation.