Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets

Hao Wu, Jie Wang, Bican Xia, Xiakun Li, Naijun Zhan, Ting Gan

TL;DR

This paper investigates nonlinear Craig interpolant synthesis for two polynomial formulas of the general form and proves the existence of a novel class of non-polynomial interpolants called semialgebraic interpolants, which is the first existence result of this kind.

Abstract

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.

Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets

TL;DR

This paper investigates nonlinear Craig interpolant synthesis for two polynomial formulas of the general form and proves the existence of a novel class of non-polynomial interpolants called semialgebraic interpolants, which is the first existence result of this kind.

Abstract

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.
Paper Structure (8 sections, 2 theorems, 8 equations)

This paper contains 8 sections, 2 theorems, 8 equations.

Table of Contents

  1. Introduction
  2. Background.
  3. Contributions.
  4. Organization.
  5. Preliminaries
  6. Quadratic Module
  7. Homogenization
  8. Problem Description

Key Result

theorem thmcountertheorem

Let $\overline{p}\coloneqq \{p_1,\ldots,p_m\}$ and $S$ be defined in eq:S. Assume that the quadratic module $\mathcal{M}(\overline{p})$ is Archimedean. If $f(\mathbf{x})> 0$ over $S$, then $f\in \mathcal{M}(\overline{p})$.

Theorems & Definitions (9)

  • definition thmcounterdefinition: Quadratic Module marshall2008book
  • definition thmcounterdefinition
  • definition thmcounterdefinition: Archimedean marshall2008book
  • theorem thmcountertheorem: Putinar's Positivstellensatz putinar93
  • proof
  • definition thmcounterdefinition
  • lemma thmcounterlemma: huang2023homogenization
  • proof
  • definition thmcounterdefinition: Interpolant