Interpolation with Automated First-Order Reasoning

TL;DR

The paper investigates interpolation within fully automated first-order theorem proving, arguing that Craig interpolation can be realized by extracting a ground interpolant from a proof and lifting it to a first-order formula. It analyzes two proof-based routes for obtaining ground interpolants—clausal tableaux and resolution—and discusses how standard preprocessing and equality encodings can be adapted to support Craig interpolation. It also connects Craig interpolation to uniform interpolation through second-order quantifier elimination, highlighting prominent algorithms such as SCAN and DLS and their historical roots. The discussion situates Craig interpolation within practical automated reasoning workflows, including proof object generation and applications in databases, logic programming, and interactive proof assistance via tools like hammers. The work thus provides both methodological foundations and a survey of enabling techniques for automated, scalable interpolation.

Abstract

We consider interpolation from the viewpoint of fully automated theorem proving in first-order logic as a general core technique for mechanized knowledge processing. For Craig interpolation, our focus is on the two-stage approach, where first an essentially propositional ground interpolant is calculated that is then lifted to a quantified first-order formula. We discuss two possibilities to obtain a ground interpolant from a proof: with clausal tableaux, and with resolution. Established preprocessing techniques for first-order proving can also be applied for Craig interpolation if they are restricted in specific ways. Equality encodings from automated reasoning justify strengthened variations of Craig interpolation. Contributions to Craig interpolation that emerged from automated reasoning include variations for logics used in databases and logic programming. As an approach to uniform interpolation we introduce second-order quantifier elimination with examples and describe the basic algorithms DLS and SCAN.