Interpolation-based techniques become popular in recent years, as they can improve the scalability of existing verification techniques due to their inherent modularity and local reasoning capabilities. Synthesizing Craig interpolants is the cornerstone of these techniques. In this paper, we investigate nonlinear Craig interpolant synthesis for two polynomial formulas of the general form, essentially corresponding to the underlying mathematical problem to separate two disjoint semialgebraic sets. By combining the homogenization approach with existing techniques, we prove the existence of a novel class of non-polynomial interpolants called semialgebraic interpolants. These semialgebraic interpolants subsume polynomial interpolants as a special case. To the best of our knowledge, this is the first existence result of this kind. Furthermore, we provide complete sum-of-squares characterizations for both polynomial and semialgebraic interpolants, which can be efficiently solved as semidefinite programs. Examples are provided to demonstrate the effectiveness and efficiency of our approach.

翻译：近年来，基于插值的技术因其固有的模块化特性和局部推理能力，能够提升现有验证技术的可扩展性，因而受到广泛关注。合成克雷格插值是这些技术的基石。本文研究了一般形式下两个多项式公式的非线性克雷格插值合成问题，其本质对应于分离两个不相交半代数集的底层数学问题。通过将齐次化方法与现有技术相结合，我们证明了一类新型非多项式插值——称为半代数插值——的存在性。这类半代数插值将多项式插值包含为其特例。据我们所知，这是此类存在性结果的首次证明。此外，我们为多项式插值和半代数插值均提供了完全的和平方表征，这些表征可以高效地作为半定规划问题求解。文中提供了示例以证明我们方法的有效性和效率。