Range-Restricted Interpolation through Clausal Tableaux
This work provides a method for query synthesis and reformulation in first-order logic, but it is incremental as it builds on existing interpolation techniques with specific structural restrictions.
The paper tackles the problem of ensuring that Craig interpolation in first-order logic preserves range-restriction and Horn properties from inputs to outputs, using clausal tableaux as the proof system. The result is a method that achieves this through a restriction of tableau structures, applicable even with resolution/paramodulation proofs, primarily for query synthesis and reformulation.
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.