Range-Restricted Interpolation through Clausal Tableaux

TL;DR

This paper introduces a method for range-restricted Craig interpolation in first-order logic using clausal tableaux, enabling applications like query reformulation and synthesis with potential for efficient implementation.

Contribution

It presents a novel approach to preserve range-restriction and Horn properties in interpolants via proof transformations within clausal tableaux, applicable to existing resolution-based proofs.

Findings

Range-restriction and Horn properties can be transferred through proof transformations.

The method is compatible with resolution and paramodulation proofs.

Potential for efficient implementation in first-order theorem provers.

Abstract

We show how variations of range-restriction and also the Horn property can be passed from inputs to outputs of Craig interpolation in first-order logic. The proof system is clausal tableaux, which stems from first-order ATP. Our results are induced by a restriction of the clausal tableau structure, which can be achieved in general by a proof transformation, also if the source proof is by resolution/paramodulation. Primarily addressed applications are query synthesis and reformulation with interpolation. Our methodical approach combines operations on proof structures with the immediate perspective of feasible implementation through incorporating highly optimized first-order provers.