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.

翻译：我们展示了在经典一阶逻辑中，通过Craig插值如何将限制区间性质以及Horn属性从输入传递到输出。证明系统采用源于经典一阶自动定理证明的子句表换。我们的结论源于对子句表换结构的限制，该限制通常可通过证明变换实现，即使原始证明基于归结/参数化方法。主要应用方向是查询合成与基于插值的查询重构。我们的方法论将证明结构操作与利用高度优化的一阶定理证明器实现可行实现的直接视角相结合。