Interpolation with Automated First-Order Reasoning

TL;DR

This paper explores automated theorem proving techniques for interpolation in first-order logic, introducing methods for ground and first-order interpolants, and proposing algorithms for second-order quantifier elimination.

Contribution

It presents new approaches for automated Craig interpolation using resolution and tableaux, and introduces algorithms for second-order quantifier elimination.

Findings

Ground interpolants can be derived from resolution and tableaux proofs.

Preprocessing techniques can be adapted for interpolation in first-order logic.

Algorithms DLS and SCAN effectively perform second-order quantifier elimination.

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.